Lazy Annotation for Program Testing and Verification

Abstract. We describe an interpolant-based approach to test generation and model checking for sequential programs. The method generates Floyd/Hoare style annotations of the program on demand, as a result of failure to achieve goals, in a manner analogous to conflict clause learning in a DPLL style SAT solver.

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Kenneth L. McMillan
• Keywords: CAV 2010, Floyd/Hoare Style Annotations, Hardware, Model Checking, Test Generation