Abstract
We present the Why/Krakatoa/Caduceus set of tools for deductive verification of Java and C source code.
This research is partly supported by ANR RNTL grant “CAT”.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (2004)
Filliâtre, J.C.: Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming 13(4), 709–745 (2003)
Couchot, J.F., Lescuyer, S.: Handling polymorphism in automated deduction. In: CADE-21, Springer, Heidelberg (2007)
Bornat, R.: Proving pointer programs in Hoare logic. In: Mathematics of Program Construction, 102–126 (2000)
Marché, C., Paulin-Mohring, C.: Reasoning about Java programs with aliasing and frame conditions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, Springer, Heidelberg (2005)
Filliâtre, J.C., Marché, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004)
Hubert, T., Marché, C.: Separation analysis for deductive verification. In: HAV 2007. Heap Analysis and Verification (2007)
Marché, C., Rousset, N.: Verification of Java Card applets behavior with respect to transactions and card tears. In: SEFM 2006, IEEE Computer Society Press, Los Alamitos (2006)
Boldo, S., Filliâtre, J.C.: Formal Verification of Floating-Point Programs. In: ARITH 2007 (2007)
Jacobs, B., Marché, C., Rauch, N.: Formal verification of a commercial smart card applet with multiple tools. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, Springer, Heidelberg (2004)
Hubert, T., Marché, C.: A case study of C source code verification: the Schorr-Waite algorithm. In: SEFM 2005, IEEE Computer Society Press, Los Alamitos (2005)
Filliâtre, J.C.: Queens on a Chessboard: an Exercise in Program Verification (2007), http://why.lri.fr/queens/
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Filliâtre, JC., Marché, C. (2007). The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds) Computer Aided Verification. CAV 2007. Lecture Notes in Computer Science, vol 4590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73368-3_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-73368-3_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73367-6
Online ISBN: 978-3-540-73368-3
eBook Packages: Computer ScienceComputer Science (R0)