| 摘要 |
A method for detecting defects in a computer program. The method steps include obtaining source code and a potential defect definition; identifying, based on the potential defect definition, a set of program objects associated with a potential defect in the source code; extracting an executable program slice having the potential defect from the source code; generating, by a processor, an abstracted model of the program slice by: modeling, using data abstraction, the set of program objects as data-abstracted variables, identifying, within the program slice, a set of control statements including predicates necessary for evaluating the set of control statements, modeling, using predicate abstraction, the predicates as predicate-abstracted Boolean variables, and creating, based on the data-abstracted variables and the predicate-abstracted Boolean variables, a finite state machine (FSM) model of the program slice; and identifying an error state of the FSM indicating an occurrence of the potential defect within the program slice. |
