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.
This work is partly supported by the ANR project U3CAT (ANR-08-SEGI-021) and the Open-DO project Hi-Lite.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)
Bobot, F., Conchon, S., Contejean, É., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo automated theorem prover (2008), http://alt-ergo.lri.fr/
Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: The Why3 platform. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.64 edn. (February 2011), http://why3.lri.fr/
Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, Wrocław, Poland (August 2011)
Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A Practical System for Verifying Concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)
Technische Universität Dresden. The world record to the n-queens puzzle (n = 26) (2009), http://queens.inf.tu-dresden.de/
The Frama-C platform for static analysis of C programs (2008), http://www.frama-c.cea.fr/
Klebanov, V., Müller, P., Shankar, N., Leavens, G.T., Wüstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Weiß, B.: The 1st Verified Software Competition: Experience report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 154–168. Springer, Heidelberg (2011), www.vscomp.org
Knuth, D.E.: The Art of Computer Programming, volume 4A: Combinatorial Algorithms, Part 1, 1st edn. Addison-Wesley Professional (2011)
Morrison, D.R.: PATRICIA—Practical Algorithm To Retrieve Information Coded in Alphanumeric. J. ACM 15(4), 514–534 (1968)
Owicki, S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM 19(5), 279–285 (1976)
The Coq Development Team. The Coq Proof Assistant Reference Manual – Version V8.3 (2010), http://coq.inria.fr
Warren, H.S.: Hackers’s Delight. Addison-Wesley (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Filliâtre, JC. (2012). Verifying Two Lines of C with Why3: An Exercise in Program Verification. In: Joshi, R., Müller, P., Podelski, A. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2012. Lecture Notes in Computer Science, vol 7152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27705-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-27705-4_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27704-7
Online ISBN: 978-3-642-27705-4
eBook Packages: Computer ScienceComputer Science (R0)