Lazy annotation for program testing and verification

84Citations
Citations of this article
55Readers
Mendeley users who have this article in their library.

This article is free to access.

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. © 2010 Springer-Verlag.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free