TY - GEN
T1 - Verifying two lines of C with Why3
T2 - 4th International Conference on Verified Software: Theories, Tool and Experiments, VSTTE 2012
AU - Filliâtre, Jean Christophe
PY - 2012/2/7
Y1 - 2012/2/7
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84856551287
U2 - 10.1007/978-3-642-27705-4_8
DO - 10.1007/978-3-642-27705-4_8
M3 - Conference contribution
AN - SCOPUS:84856551287
SN - 9783642277047
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 83
EP - 97
BT - Verified Software
Y2 - 28 January 2012 through 29 January 2012
ER -