Article

A certified multi-prover verification condition generator

Authors:

Claude Marché,

Benjamin MonateAuthors Info & Claims

VSTTE'12: Proceedings of the 4th international conference on Verified Software: theories, tools, experiments

Pages 2 - 17

https://doi.org/10.1007/978-3-642-27705-4_2

Published: 28 January 2012 Publication History

Abstract

Deduction-based software verification tools have reached a maturity allowing them to be used in industrial context where a very high level of assurance is required. This raises the question of the level of confidence we can grant to the tools themselves. We present a certified implementation of a verification condition generator. An originality is its genericity with respect to the logical context, which allows us to produce proof obligations for a large class of theorem provers.

References

[1]

Abrial, J.-R.: The B-Book, assigning programs to meaning. Cambridge University Press (1996).

Digital Library

[2]

Barnett, M., DeLine, R., Jacobs, B., Chang, B.-Y.E., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364-387. Springer, Heidelberg (2006).

Digital Library

[3]

Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49-69. Springer, Heidelberg (2005).

Digital Library

[4]

Baudin, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language, version 1.4 (2009), http://frama-c.cea.fr/acsl.html

[5]

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004).

Digital Library

[6]

Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First InternationalWorkshop on Intermediate Verification Languages, Wroclaw, Poland (August 2011).

[7]

Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer (STTT) 7(3), 212-232 (2005).

Digital Library

[8]

Chlipala, A.: Certified Programming with Dependent Types. MIT Press (2011), http://adam.chlipala.net/cpdt/

[9]

Chlipala, A.J., Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: Hutton, G., Tolmach, A.P. (eds.) ICFP, pp. 79-90. ACM, Edinburgh (2009).

Digital Library

[10]

Cok, D.R., Kiniry, J.R.: ESC/Java2: Uniting eSC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108-128. Springer, Heidelberg (2005).

Digital Library

[11]

Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: Contractbased modular verification of concurrent C. In: 31st International Conference on Software Engineering Companion, ICSE 2009, Vancouver, Canada, May 16-24, pp. 429-430. IEEE Comp. Soc. Press (2009).

[12]

Filliâtre, J.-C.: Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming 13(4), 709-745 (2003).

Digital Library

[13]

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).

[14]

Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173-177. Springer, Heidelberg (2007).

Digital Library

[15]

Herms, P.: Certification of a chain for deductive program verification. In: Bertot, Y. (ed.) 2nd Coq Workshop, Satellite of ITP 2010 (2010).

[16]

Herms, P., Marché, C., Monate, B.: A certified multi-prover verification condition generator. Research Report 7793, INRIA (2011), http://hal.inria.fr/hal-00639977/en/

[17]

Homeier, P.V., Martin, D.F.: A mechanically verified verification condition generator. The Computer Journal 38(2), 131-141 (1995).

[18]

Homeier, P.V., Martin, D.F.: Mechanical Verification of Mutually Recursive Procedures. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 201-215. Springer, Heidelberg (1996).

Digital Library

[19]

Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43(4), 363-446 (2009).

Digital Library

[20]

Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207, 284-304 (2009).

Digital Library

[21]

Lescuyer, S.: Formalisation et développement d'une tactique réflexive pour la démonstration automatique en Coq. Thèse de doctorat, Université Paris-Sud (2011).

[22]

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

[23]

Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Reasoning with the awkward squad. In: Proceedings of ICFP 2008(2008).

[24]

Norrish, M.: C Formalised in HOL. PhD thesis, University of Cambridge (November 1998).

[25]

Randimbivololona, F., Souyris, J., Baudin, P., Pacalet, A., Raguideau, J., Schoen, D.: Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1798-1815. Springer, Heidelberg (1999).

Digital Library

[26]

Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technische Universität München (2006).

[27]

Wagner, M., Bormer, T.: Testing a verifying compiler. In: Beckert, B., Marché, C. (eds.) Formal Verification of Object-Oriented Software, Papers Presented at the International Conference, Karlsruhe Reports in Informatics, Paris (2010), http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083

Cited By

Zimmerman CDiVincenzo JAldrich J(2024)Sound Gradual Verification with Symbolic ExecutionProceedings of the ACM on Programming Languages10.1145/36329278:POPL(2547-2576)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632927
Cohen JJohnson-Freyd P(2024)A Formalization of Core Why3 in CoqProceedings of the ACM on Programming Languages10.1145/36329028:POPL(1789-1818)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632902
Blanchard AKosmatov NLoulergue FHung CPapadopoulos G(2019)Logic against ghostsProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297495(2186-2195)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297495
Show More Cited By

A certified multi-prover verification condition generator

Recommendations

Formally Validating a Practical Verification Condition Generator
Computer Aided Verification
Abstract
A program verifier produces reliable results only if both the logic used to justify the program’s correctness is sound, and the implementation of the program verifier is itself correct. Whereas it is common to formally prove soundness of the logic,...
A machine-checked soundness proof for an efficient verification condition generator
SAC '10: Proceedings of the 2010 ACM Symposium on Applied Computing

Verification conditions (VCs) are logical formulae whose validity implies the correctness of a program with respect to a specification. The technique of checking software properties by specifying them in a program logic, then generating VCs, and finally ...
The verification of mdg algorithms in the hol theorem prover

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

VSTTE'12: Proceedings of the 4th international conference on Verified Software: theories, tools, experiments

January 2012

326 pages

ISBN:9783642277047

Editors:
Rajeev Joshi
MS 301-285, 4800 Oak Grove Drive, Pasadena, CA
,
Peter Müller
ETH Zürich, Universitätstr. 6, Zürich, CA, Switzerland
,
Andreas Podelski
Department of Computer Science, University of Freiburg, Georges-Köhler-Allee 52, Freiburg, CA, Germany

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 28 January 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zimmerman CDiVincenzo JAldrich J(2024)Sound Gradual Verification with Symbolic ExecutionProceedings of the ACM on Programming Languages10.1145/36329278:POPL(2547-2576)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632927
Cohen JJohnson-Freyd P(2024)A Formalization of Core Why3 in CoqProceedings of the ACM on Programming Languages10.1145/36329028:POPL(1789-1818)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632902
Blanchard AKosmatov NLoulergue FHung CPapadopoulos G(2019)Logic against ghostsProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297495(2186-2195)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297495
Fromherz AGiannarakis NHawblitzel CParno BRastogi ASwamy N(2019)A verified, efficient embedding of a verifiable assembly languageProceedings of the ACM on Programming Languages10.1145/32903763:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290376
Lourenço CFrade MPinto JGnesi SPlat NDay NRossi M(2019)A generalized program verification workflow based on loop elimination and SA formProceedings of the 7th International Workshop on Formal Methods in Software Engineering10.1109/FormaliSE.2019.00017(75-84)Online publication date: 27-May-2019
https://dl.acm.org/doi/10.1109/FormaliSE.2019.00017
Kirchner FKosmatov NPrevosto VSignoles JYakobowski B(2018)Frama-CFormal Aspects of Computing10.1007/s00165-014-0326-727:3(573-609)Online publication date: 27-Dec-2018
https://dl.acm.org/doi/10.1007/s00165-014-0326-7
Jourdan JLaporte VBlazy SLeroy XPichardie D(2015)A Formally-Verified C Static AnalyzerACM SIGPLAN Notices10.1145/2775051.267696650:1(247-259)Online publication date: 14-Jan-2015
https://dl.acm.org/doi/10.1145/2775051.2676966
Jourdan JLaporte VBlazy SLeroy XPichardie DRajamani SWalker D(2015)A Formally-Verified C Static AnalyzerProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2676726.2676966(247-259)Online publication date: 14-Jan-2015
https://dl.acm.org/doi/10.1145/2676726.2676966

View Options

View options

Figures

Tables

Media

View Table of Conten