Efficient model checking technique for finding software defects

A non-transitory computer-readable storage medium storing a plurality of instructions for detecting defects in a computer program, the plurality of instructions comprising functionality to:

• obtain a plurality of source code and a potential defect definition;
• identify, based on the potential defect definition, a plurality of program objects associated with a potential defect in the plurality of source code;
• extract an executable program slice having the potential defect from the plurality of source code;
• generate an abstracted model of the program slice by:
• modeling, using data abstraction, the plurality of program objects as a plurality of data-abstracted variables that represent a reduced set of possible states of the plurality of program objects,
• identifying, within the program slice, a first plurality of control statements comprising a first plurality of predicates necessary for evaluating the first plurality of control statements,
• modeling, using predicate abstraction, the plurality of predicates as a plurality of predicate-abstracted Boolean variables that represent a reduced set of possible states of the first plurality of control statements, and
• creating, based on the plurality of data-abstracted variables and the plurality of predicate-abstracted Boolean variables, a finite state machine (FSM) model of the program slice;
• and
• identify an error state of the FSM indicating an occurrence of the potential defect within the program slice.

A system for detecting defects in a computer program, comprising:

• a processor;
• a defect analysis tool executing on the processor and configured to:
• obtain a plurality of source code and a potential defect definition,
• identify, based on the potential defect definition, a plurality of program objects associated with a potential defect in the plurality of source code;
• extract an executable program slice having the potential defect from the plurality of source code;
• a model generator executing on the processor and configured to generate an abstracted model of the program slice by:
• modeling, using data abstraction, the plurality of program objects as a plurality of data-abstracted variables that represent a reduced set of possible states of the plurality of program objects,
• identifying, within the program slice, a first plurality of control statements comprising a first plurality of predicates necessary for evaluating the first plurality of control statements,
• modeling, using predicate abstraction, the plurality of predicates as a plurality of predicate-abstracted Boolean variables that represent a reduced set of possible states of the first plurality of control statements, and
• creating, based on the plurality of data-abstracted variables and the plurality of predicate-abstracted Boolean variables, a finite state machine (FSM) model of the program slice;
• and
• a model checker executing on the processor and configured to:
• identify an error state of the FSM indicating an occurrence of the potential defect within the program slice.