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.
"Lazy Annotation for Program Testing and Verification"
Kenneth McMillan
In Proceedings of Computer Aided Verification, Edinburgh, UK, July 15-19, 2010.
@incollection {springerlink:10.1007/978-3-642-14295-6_10,
author = {McMillan, Kenneth},
affiliation = {Cadence Berkeley Labs},
title = {Lazy Annotation for Program Testing and Verification},
booktitle = {Computer Aided Verification},
series = {Lecture Notes in Computer Science},
editor = {Touili, Tayssir and Cook, Byron and Jackson, Paul},
publisher = {Springer Berlin / Heidelberg},
isbn = {},
pages = {104-118},
volume = {6174},
url = {http://dx.doi.org/10.1007/978-3-642-14295-6_10},
note = {10.1007/978-3-642-14295-6_10},
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.},
year = {2010}
}