Abstract
Our goal is the verification of C programs at the source code level using formal proof tools. Programs are specified using annotations such as pre- and post-conditions and global invariants. An original approach is presented which allows to formally prove that a function implementation satisfies its specification and is free of null pointer dereferencing and out-of-bounds array access. The method is not bound to a particular back-end theorem prover. A significant part of the ANSI C language is supported, including pointer arithmetic and possible pointer aliasing. We describe a prototype tool and give some experimental results.
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.
Similar content being viewed by others
References
The Simplify decision procedure (part of ESC/Java), http://research.compaq.com/SRC/esc/simplify/
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE static analyzer, http://www.astree.ens.fr/
Bornat, R.: Proving pointer programs in Hoare logic. In: Mathematics of Program Construction, pp. 102–126 (2000)
Burstall, R.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence 7, 23–50, 72
CAVEAT project, http://www-drt.cea.fr/Pages/List/lse/LSL/Caveat/index.html
Cook, B.: Static driver verifier, http://www.microsoft.com/whdc/devtools/tools/sdv.mspx
The Coq Proof Assistant, http://coq.inria.fr/
Cousot, P.: Methods and logics for proving programs. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 841–993. North-Holland, Amsterdam (1990)
Filliâtre, J.-C.: Verification of Non-Functional Programs using Interpretations in Type Theory. Journal of Functional Programming 13(4), 709–745 (2003)
Filliâtre, J.-C.: The why verification tool (2002)
Filliâtre, J.-C., Marché, C.: The Caduceus tool for the verification of C programs, http://why.lri.fr/caduceus/
Kaplan, D.: Some Completeness Results in the Mathematical Theory of Computation. J. ACM 15(1), 124–134 (1968)
Kernighan, B., Ritchie, D.: The C Programming Language, 2nd edn. Prentice-Hall, Englewood Cliffs (1988)
Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: notations and tools supporting detailed design in Java. In: OOPSLA 2000 Companion, Minneapolis, Minnesota, pp. 105–106 (2000)
Marché, C., Paulin, C., Urbain, X.: The KRAKATOA proof tool (2002), http://krakatoa.lri.fr/
Marché, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming 58(1–2), 89–106 (2004), http://krakatoa.lri.fr
Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) 19th Conference on Automated Deduction. LNCS. Springer, Heidelberg (2003)
The PVS system, http://pvs.csl.sri.com/
Ranise, S., Deharbe, D.: Light-weight theorem proving for debugging and verifying units of code. In: Proc. SEFM 2003, Canberra, Australia, September 2003. IEEE Computer Society Press, Canberra (2003), http://www.loria.fr/equipes/cassis/softwares/haRVey/
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: 17h Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos (2002)
Sun Microsystems. The JavaCardTM application programming interface (API), http://java.sun.com/products/javacard/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Filliâtre, JC., Marché, C. (2004). Multi-prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds) Formal Methods and Software Engineering. ICFEM 2004. Lecture Notes in Computer Science, vol 3308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30482-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-30482-1_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23841-6
Online ISBN: 978-3-540-30482-1
eBook Packages: Springer Book Archive