Active property checking

13 years 9 months ago
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...
Patrice Godefroid, Michael Y. Levin, David A. Moln
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Authors Patrice Godefroid, Michael Y. Levin, David A. Molnar
Comments (0)