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. © 2010 Springer-Verlag.
CITATION STYLE
McMillan, K. L. (2010). Lazy annotation for program testing and verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6174 LNCS, pp. 104–118). https://doi.org/10.1007/978-3-642-14295-6_10
Mendeley helps you to discover research relevant for your work.