Active property checking

Runtime property checking (as implemented in tools like Purify or Valgrind) checks whether a program execution satisfies a property. Active property checking extends runtime checking by checking whether the property is satisfied by all program executions that follow the same program path. This check is performed on a symbolic execution of the given program path using a constraint solver. If the check fails, the constraint solver generates an alternative program input triggering a new program execution that follows the same program path but exhibits a property violation. Combined with systematic dynamic test generation, which attempts to exercise all feasible paths in a program, active property checking defines a new form of dynamic software model checking (program verification). In this paper, we formalize and study active property checking. We show how static and dynamic type checking can be extended with active type checking. Then, we discuss how to implement active property checkin...

• Type: Conference
• Year: 2008
• Where: EMSOFT
• Authors: Patrice Godefroid, Michael Y. Levin, David A. Molnar
• Keywords: Active Property Checking, EMSOFT 2008, Program Execution, Property Checking, Software Engineering