Abstract
This article details the formal verification of a 2-line C program that computes the number of solutions to the n-queens problem. The formal proof of (an abstraction of) the C code is performed using the Why3 tool to generate the verification conditions and several provers (Alt-Ergo, CVC3, Coq) to discharge them. The main purpose of this article is to illustrate the use of Why3 in verifying an algorithmically complex program. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Filliâtre, J. C. (2012). Verifying two lines of C with Why3: An exercise in program verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7152 LNCS, pp. 83–97). https://doi.org/10.1007/978-3-642-27705-4_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
