@inproceedings{aa2905315e2f429eab67aa911ea72114,
title = "Verifying two lines of C with Why3: An exercise in program verification",
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.",
author = "Filli{\^a}tre, \{Jean Christophe\}",
year = "2012",
month = feb,
day = "7",
doi = "10.1007/978-3-642-27705-4\_8",
language = "English",
isbn = "9783642277047",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "83--97",
booktitle = "Verified Software",
note = "4th International Conference on Verified Software: Theories, Tool and Experiments, VSTTE 2012 ; Conference date: 28-01-2012 Through 29-01-2012",
}