SpringerLink
Log in

Formally Verifying that a Program Does What It Should: The Wp Plug-in

  • Chapter
  • First Online:
Guide to Software Verification with Frama-C

Part of the book series: Computer Science Foundations and Applied Logic ((CSFAL))

  • 23 Accesses

Abstract

This chapter presents how to prove ACSL properties of C programs with the Wp plug-in of Frama-C using deductive verification and SMT solvers or Proof Assistants. Specifically, this chapter explores the internals of the Wp plug-in, with a specific focus on how ACSL and C are encoded into classical first-order logic, including its various memory models. Then, the internal proof strategy of Wp is described, which leads to a discussion on specification methodology and proof engineering, and how to interact with the Wp plug-in. Finally, we compare Wp with a selection of other amazing systems and logics for the deductive verification of C programs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 69.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    This Wp simplifier actually reuses the Eva abstract domains for this purpose.

  2. 2.

    These resources are also available from the Wp pages of the Frama-C website: https://www.frama-c.com/fc-plugins/wp.html, https://www.frama-c.com/html/publications.html#wp.

References

  1. Abrial JR, Hoare A, Chapron P (1996) The B-Book: assigning programs to meanings. Cambridge University Press. https://doi.org/10.1017/CBO9780511624162

  2. Ahrendt W, Beckert B, Bubel R, Hähnle R, Schmitt PH, Ulbrich M (eds) Deductive software verification—the KeY Book—from theory to practice. Lecture notes in computer science, vol 10001. Springer (2016). https://doi.org/10.1007/978-3-319-49812-6

  3. Barbosa H, Barrett CW, Brain M, Kremer G, Lachnitt H, Mann M, Mohamed A, Mohamed M, Niemetz A, Nötzli A, Ozdemir A, Preiner M, Reynolds A, Sheng Y, Tinelli C, Zohar Y (2022) CVC5: a versatile and industrial-strength SMT solver. In: Fisman D, Rosu G (eds) Proceedings of the tools and algorithms for the construction and analysis of systems—28th international conference, TACAS 2022. Lecture notes in computer science, vol 13243. Springer (2022), pp 415–442. https://doi.org/10.1007/978-3-030-99524-9_24

  4. Barrett CW, Conway CL, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C (2011) CVC4. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of the computer aided verification—23rd international conference, CAV 2011. Lecture notes in computer science, vol 6806. Springer, pp 171–177. https://doi.org/10.1007/978-3-642-22110-1_14

  5. Baudin P, Cuoq P, Filliâtre JC, Marché C, Monate B, Moy Y, Prevosto V (2020) ACSL: ANSI/ISO C specification language, version 1.16. https://frama-c.com/html/acsl.html

  6. Baudin P, Pacalet A, Raguideau J, Schoen D, Williams N (2002) CAVEAT: a tool for software validation. In: Proceedings of the international conference on dependable systems and networks DSN 2002 , p 537. Bethesda, USA (2002). https://doi.org/10.1109/DSN.2002.1028953

  7. Bertot Y (2016) Coq in a hurry. https://cel.hal.science/inria-00001173. Lecture

  8. Beyer D, Henzinger TA, Jhala R, Majumdar R (2007) The software model checker blast. Int J Softw Tools Technoly Trans 9(5–6):505–525. https://doi.org/10.1007/s10009-007-0044-z

    Article  Google Scholar 

  9. Beyer D, Keremoglu ME (2011) CPAchecker: a tool for configurable software verification. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of the computer aided verification—23rd international conference, CAV 2011. Lecture notes in computer science, vol 6806. Springer, pp 184–190. https://doi.org/10.1007/978-3-642-22110-1_16

  10. Beyer D, Spiessl M, Umbricht S (2022) Cooperation between automatic and interactive software verifiers. In: Proceedings of the software engineering and formal methods—20th international conference, SEFM 2022. Lecture notes in computer science, vol 13550. Springer, pp 111–128. https://doi.org/10.1007/978-3-031-17108-6_7

  11. Blanchard A (2020) Introduction to C program proof with Frama-C and its WP plugin. https://allan-blanchard.fr/frama-c-wp-tutorial.html

  12. Blanchard A, Loulergue F, Kosmatov N (2019) Towards full proof automation in Frama-C using auto-active verification. In: Badger JM, Rozier KY (eds) Proceedings of the NASA formal methods—11th international symposium, NFM 2019. Lecture notes in computer science, vol 11460. Springer, pp 88–105. https://doi.org/10.1007/978-3-030-20652-9_6

  13. Bloch J (2006) Nearly all binary searches and mergesorts are broken. https://ai.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html

  14. Bobot F, Filliâtre JC, Marché C, Paskevich A (2011) Why3: shepherd your herd of provers. In: Boogie 2011: first international workshop on intermediate verification languages. https://hal.inria.fr/hal-00790310

  15. Bornat R (2000) Proving pointer programs in hoare logic. In: Proceedings of the mathematics of program construction—5th international conference, MPC 2000. Lecture notes in computer science, vol 1837. Springer, pp 102–126. https://doi.org/10.1007/10722010_8

  16. Brahmi A, Delmas D, Essoussi MH, Randimbivololona F, Atki A, Marie T (2018) Formalise to automate: deployment of a safe and cost-efficient process for avionics software. In: Embedded real time software and systems—9th european congress, ERTS 2018

    Google Scholar 

  17. Cao Q, Beringer L, Gruetter S, Dodds J, Appel AW (2018) VST-Floyd: a separation logic tool to verify correctness of C programs. J Autom Reason 61(1–4):367–422. https://doi.org/10.1007/s10817-018-9457-5

    Article  MathSciNet  Google Scholar 

  18. Comar C, Kanig J, Moy Y (2012) Integrating formal program verification with testing. In: Embedded real time software and systems—6th European congress, ERTS 2012. Toulouse, France. https://hal.archives-ouvertes.fr/hal-02263435

  19. Conchon S, Coquereau A, Iguernlala M, Mebsout A (2018) Alt-Ergo 2.2. In: SMT workshop: international workshop on satisfiability modulo theories. https://hal.inria.fr/hal-01960203

  20. Correnson L (2014) Qed. Computing what remains to be proved. In: Proceedings of the NASA formal methods—6th international symposium, NFM 2014. Lecture notes in computer science, vol 8430. Springer, pp 215–229. https://doi.org/10.1007/978-3-319-06200-6_17

  21. Dahlweid M, Moskal M, Santen T, Tobies S, Schulte W (2009) VCC: contract-based modular verification of concurrent C. In: 31st international conference on software engineering, ICSE 2009. Companion volume. IEEE. https://doi.org/10.1109/ICSE-COMPANION.2009.5071046

  22. Dams D, Namjoshi KS (2003) Shape analysis through predicate abstraction and model checking. In: Proceedings of the verification, model checking, and abstract interpretation, 4th international conference, VMCAI 2003. Lecture notes in computer science, vol 2575. Springer, pp 310–324. https://doi.org/10.1007/3-540-36384-X_25

  23. Djoudi A, Hána M, Kosmatov N (2021) Formal verification of a JavaCard virtual machine with Frama-C. In: Huisman M, Pasareanu CS, Zhan N (eds) Proceedings of the formal methods—24th international symposium, FM 2021. Lecture notes in computer science, vol 13047, pp 427–444. Springer. https://doi.org/10.1007/978-3-030-90870-6_23

  24. Ebalard A, Mouy P, Benadjila R (2019) Journey to a RTE-free X.509 parser. Symposium sur la sécurité des technologies de l’information et des communications (SSTIC)

    Google Scholar 

  25. Filliâtre J (2011) Deductive software verification. Int J Softw Tools Technol Trans 13(5):397–403. https://doi.org/10.1007/s10009-011-0211-0

    Article  Google Scholar 

  26. Filliâtre J, Marché C (2007) The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm W, Hermanns H (eds) Proceedings computer aided verification, 19th international conference, CAV 2007. Lecture notes in computer science, vol 4590. Springer, pp 173–177. https://doi.org/10.1007/978-3-540-73368-3_21

  27. Gentzen G (1935) Untersuchungen über das logische Schließen I. Mathematische Zeitschrift 39:176–210

    Article  MathSciNet  Google Scholar 

  28. Gerlach J (2019) Minimal Contract Hoare-Style Verification versus Abstract Interpretation. Technical report, Fraunhofer FOKUS. VESSEDIA Project

    Google Scholar 

  29. Gerlach J (2020) ACSL by Example. Tutorial, Fraunhofer FOKUS. https://github.com/fraunhoferfokus/acsl-by-example

  30. Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580. https://doi.org/10.1145/363235.363259

    Article  Google Scholar 

  31. Hoenicke J, Leino KRM, Podelski A, Schäf M, Wies T (2009) It’s doomed; we can prove it. In: Proceedings of the formal methods—2nd workd congress, FM 2009. Lecture notes in computer science, vol 5850. Springer, pp 338–353. https://doi.org/10.1007/978-3-642-05089-3_22

  32. Hubert T, Marché C (2007) Separation analysis for weakest precondition-based verification. In: HAV 2007—heap analysis and verification, pp 81–93. https://hal.inria.fr/hal-03630177

  33. Jacobs B, Smans J, Philippaerts P, Vogels F, Penninckx W, Piessens F (2011) VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru MG, Havelund K, Holzmann GJ, Joshi R (eds) Proceedings of the NASA formal methods—3rd international symposium, NFM 2011. Lecture notes in computer science, vol 6617. Springer. https://doi.org/10.1007/978-3-642-20398-5_4

  34. Klein G, Andronick J, Elphinstone K, Heiser G, Cock DA, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S (2010) seL4: formal verification of an operating-system kernel. Commun ACM 53(6):107–115. https://doi.org/10.1145/1743546.1743574

    Article  Google Scholar 

  35. Leino KRM (2005) Efficient weakest preconditions. Inf Proc Lett 93(6):281–288. https://doi.org/10.1016/j.ipl.2004.10.015

    Article  MathSciNet  Google Scholar 

  36. Leino KRM, Moskal M (2010) Usable auto-active verification. http://fm.csl.sri.com/UV10/

  37. Leroy X (2009) Formal verification of a realistic compiler. Commun ACM 52(7):107–115. https://doi.org/10.1145/1538788.1538814

    Article  Google Scholar 

  38. Maksimovic P, Ayoun S, Santos JF, Gardner P (2021) Gillian, Part II: real-world verification for JavaScript and C. In: Silva A, Leino KRM (eds) Proceedings of the computer aided verification—33rd international conference, CAV 2021. Lecture notes in computer science, vol 12760. Springer, pp 827–850. https://doi.org/10.1007/978-3-030-81688-9_38

  39. de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Proceedings of the tools and algorithms for the construction and analysis of systems—14th international conference, TACAS 2008, vol 4963, pp 337–340. https://doi.org/10.1007/978-3-540-78800-3_24

  40. Nicole O, Lemerre M, Rival X (2022) Lightweight shape analysis based on physical types. In: Finkbeiner B, Wies T (eds) Proceedings of the verification, model checking, and abstract interpretation—23rd international conference, VMCAI 2022. Lecture notes in computer science, vol 13182. Springer, pp 219–241. https://doi.org/10.1007/978-3-030-94583-1_11

  41. Protzenko J, Zinzindohoué JK, Rastogi A, Ramananandro T, Wang P, Béguelin SZ, Delignat-Lavaud A, Hritcu C, Bhargavan K, Fournet C, Swamy N (2017) Verified low-level programming embedded in F*. Proceedings of the 22nd international conference on functional programming, ICFP 2017, vol 1, pp 17:1–17:29 (2017). https://doi.org/10.1145/3110261

  42. Rieu-Helft R (2019) A Why3 proof of GMP algorithms. J Form Reas 12(1):53–97. https://doi.org/10.6092/issn.1972-5787/9730

    Article  MathSciNet  Google Scholar 

  43. Rosen BK, Wegman MN, Zadeck FK (1988) Global value numbers and redundant computations. In: Ferrante J, Mager P (eds) Conference record of the 15th annual ACM symposium on principles of programming languages, POPL 1988. ACM Press, pp 12–27. https://doi.org/10.1145/73560.73562

  44. Sammler M, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D (2021) RefinedC: automating the foundational verification of C code with refined ownership types. In: Freund SN, Yahav E (eds) Programming language design and implementation—42nd international conference, PLDI 2021. ACM, pp 158–174. https://doi.org/10.1145/3453483.3454036

  45. Santos JF, Maksimovic P, Ayoun S, Gardner P (2020) Gillian, Part I: a multi-language platform for symbolic execution. In: Donaldson AF, Torlak E (eds) Proceedings of the programming language design and implementation—41st international conference, PLDI 2020. ACM, pp 927–942. https://doi.org/10.1145/3385412.3386014

  46. Turing AM (1937) On computable numbers, with an application to the entscheidungsproblem. In: Proceedings of the London mathematical society, vol s2-42(1), pp 230–265. https://doi.org/10.1112/plms/s2-42.1.230

  47. Volkov G, Mandrykin M, Efremov D (2018) Lemma functions for Frama-C: C programs as proofs. In: Proceedings of the 2018 Ivannikov ISPRAS open conference (ISPRAS-2018), pp 31–38. https://doi.org/10.1109/ISPRAS.2018.00012

Download references

Acknowledgements

The authors would like to warmly cite the other main contributors of Wp, namely Anne Pacalet who was at the very origin of the project, Zaynah Dargaye who contributed to the early design of Wp memory models, and to thank all the Frama-C kernel developers for their support. The authors also thank the anonymous reviewers who provided numerous helpful comments and questions that allowed to greatly improve this chapter.

Author information

Authors and Affiliations

  1. Université Paris-Saclay, CEA, List, Palaiseau, France

    Allan Blanchard, François Bobot, Patrick Baudin & Loïc Correnson

Authors
  1. Allan Blanchard
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. François Bobot
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Patrick Baudin
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Loïc Correnson
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Allan Blanchard .

Editor information

Editors and Affiliations

  1. Thales Research & Technology, Palaiseau, France

    Nikolai Kosmatov

  2. Software Safety and Security Laboratory, Université Paris-Saclay, CEA, List, Gif-sur-Yvette, France

    Virgile Prevosto

  3. Software Safety and Security Laboratory, Université Paris-Saclay, CEA, List, Gif-sur-Yvette, France

    Julien Signoles

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Blanchard, A., Bobot, F., Baudin, P., Correnson, L. (2024). Formally Verifying that a Program Does What It Should: The Wp Plug-in. In: Kosmatov, N., Prevosto, V., Signoles, J. (eds) Guide to Software Verification with Frama-C. Computer Science Foundations and Applied Logic. Springer, Cham. https://doi.org/10.1007/978-3-031-55608-1_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-55608-1_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-55607-4

  • Online ISBN: 978-3-031-55608-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation