Skip to main content
SpringerLink
Log in

Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques (ISoLA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9952))

Included in the following conference series:

Abstract

Why3 is an environment for static verification, generic in the sense that it is used as an intermediate tool by different front-ends for the verification of Java, C or Ada programs. Yet, the choices made when designing the specification languages provided by those front-ends differ significantly, in particular with respect to the executability of specifications. We review these differences and the issues that result from these choices. We emphasize the specific feature of ghost code which turns out to be extremely useful for both static and dynamic verification. We also present techniques, combining static and dynamic features, that help users understand why static verification fails.

Work partly supported by the Joint Laboratory ProofInUse (ANR-13-LAB3-0007, http://www.spark-2014.org/proofinuse) of the French national research organization.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Barnes, J.: Programming in Ada 2012. Cambridge University Press, Cambridge (2014)

    Book  Google Scholar 

  2. 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). doi:10.1007/978-3-540-30569-9_3

    Chapter  Google Scholar 

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

  4. Bulwahn, L.: The new quickcheck for Isabelle. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 92–108. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  5. 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. Intl. J. Softw. Tools Technol. Transf. 7(3), 212–232 (2005)

    Article  Google Scholar 

  6. Burghardt, J., Gerlach, J., Lapawczyk, T., Carben, A., Gu, L., Hartig, K., Pohl, H., Soto, J., Völlinger, K.: ACSL by example, towards a verified C standard library. Version 11.11 for Frama-C Sodium. Technical report, Fraunhofer FOKUS (2015). http://publica.fraunhofer.de/dokumente/N-364387.html

  7. Chalin, P.: Logical foundations of program assertions: what do practitioners want? In: SEFM, pp. 383–393. IEEE Computer Society (2005)

    Google Scholar 

  8. Chalin, P.: Reassessing JML’s logical foundation. In: Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP 2005), Glasgow, Scotland (2005)

    Google Scholar 

  9. Chapman, R., Schanda, F.: Are we there yet? 20 years of industrial theorem proving with SPARK. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 17–26. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08970-6_2

    Google Scholar 

  10. Christakis, M., Leino, K.R.M., Müller, P., Wüstholz, V.: Integrated environment for diagnosing verification errors. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 424–441. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_25

    Chapter  Google Scholar 

  11. Clochard, M.: Automatically verified implementation of data structures based on AVL trees. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 167–180. Springer, Heidelberg (2014)

    Google Scholar 

  12. Clochard, M., Filliâtre, J.-C., Marché, C., Paskevich, A.: Formalizing semantics with an automatic program verifier. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 37–51. Springer, Heidelberg (2014). doi:10.1007/978-3-319-12154-3_3

    Google Scholar 

  13. Clochard, M., Marché, C., Paskevich, A.: Verified programs with binders. In: Programming Languages meets Program Verification (PLPV). ACM Press (2014)

    Google Scholar 

  14. Cok, D.R.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: F-IDE 2014. EPTCS 149, pp. 79–92 (2014)

    Google Scholar 

  15. Correnson, L., Signoles, J.: Combining analyses for C program verification. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 108–130. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32469-7_8

    Chapter  Google Scholar 

  16. Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: SAC, pp. 1230–1235. ACM (2013)

    Google Scholar 

  17. Dross, C., Filliâtre, J.-C., Moy, Y.: Correct code containing containers. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 102–118. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21768-5_9

    Chapter  Google Scholar 

  18. Dross, C., Moy, Y.: Abstract software specifications and automatic proof of refinement. In: RSSR (2016). http://www.spark-2014.org/entries/detail/spark-prez-at-new-conference-on-railway-systems

  19. Dufour, J.L.: B extended to floating-point numbers: is it sufficient for proving avionics software? In: Formal Methods Applied to Complex Systems. Wiley (2014)

    Google Scholar 

  20. Filliâtre, J.C., Gondelman, L., Paskevich, A.: The spirit of ghost code. In: Formal Methods in System Design (2016, to appear)

    Google Scholar 

  21. 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). doi:10.1007/978-3-540-30482-1_10

    Chapter  Google Scholar 

  22. 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). doi:10.1007/978-3-540-73368-3_21

    Chapter  Google Scholar 

  23. Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  24. Gao, S., Avigad, J., Clarke, E.M.: Delta-complete decision procedures for satisfiability over the reals. CoRR abs/1204.3513 (2012). http://arxiv.org/abs/1204.3513

  25. GMP: GNU multiple precision arithmetic library. https://gmplib.org/

  26. Hauzar, D., Marché, C., Moy, Y.: Counter examples from proof failures in SPARK. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 215–233. Springer, Heidelberg (2016). doi:10.1007/978-3-319-41591-8_15

    Chapter  Google Scholar 

  27. 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, pp. 241–257. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27815-3_21

    Chapter  Google Scholar 

  28. Jakobsson, A., Kosmatov, N., Signoles, J.: Rester statique pour devenir plus rapide, plus précis et plus mince. In: JFLA (2015)

    Google Scholar 

  29. Kanig, J., Chapman, R., Comar, C., Guitton, J., Moy, Y., Rees, E.: Explicit assumptions - a prenup for marrying static and dynamic program verification. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 142–157. Springer, Heidelberg (2014). doi:10.1007/978-3-319-09099-3_11

    Google Scholar 

  30. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects of Computing, pp. 1–37 (2015)

    Google Scholar 

  31. Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: OOPSLA, pp. 407–426. ACM (2013)

    Google Scholar 

  32. Kosmatov, N., Petiot, G., Signoles, J.: An optimized memory monitoring for runtime assertion checking of C programs. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 167–182. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40787-1_10

    Chapter  Google Scholar 

  33. Kosmatov, N., Signoles, J.: A lesson on runtime assertion checking with Frama-C. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 386–399. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40787-1_29

    Chapter  Google Scholar 

  34. Kosmatov, N., Signoles, J.: Runtime assertion checking and its combinations with static and dynamic analyses. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 165–168. Springer, Heidelberg (2014). doi:10.1007/978-3-319-09099-3_13

    Google Scholar 

  35. Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accomodates both runtime assertion checking and formal verification. Technical report 03-04, Iowa State University (2003)

    Google Scholar 

  36. Leino, K.R.M.: Automating induction with an SMT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 315–331. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27940-9_21

    Chapter  Google Scholar 

  37. Leino, K.R.M., Wüstholz, V.: The Dafny integrated development environment. In: F-IDE. Electronic Proceedings in Theoretical Computer Science, vol. 149, pp. 3–15 (2014)

    Google Scholar 

  38. Marché, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. J. Logic Algebraic Program. 58(1–2), 89–106 (2004)

    Article  MATH  Google Scholar 

  39. McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)

    Book  MATH  Google Scholar 

  40. Meyer, B.: Object-Oriented Software Construction, 1st edn. Prentice-Hall Inc., Upper Saddle River (1988)

    MATH  Google Scholar 

  41. Petiot, G., Kosmatov, N., Botella, B., Giorgetti, A., Julliand, J.: Your proof fails? Testing helps to find the reason. In: Aichernig, B.K.K., Furia, C.A.A. (eds.) TAP 2016. LNCS, vol. 9762, pp. 130–150. Springer, Heidelberg (2016). doi:10.1007/978-3-319-41135-4_8

    Chapter  Google Scholar 

  42. Signoles, J.: Software architecture of code analysis frameworks matters: the Frama-C example. In: F-IDE, pp. 86–96 (2015)

    Google Scholar 

  43. Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Program checking with less hassle. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 149–169. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54108-7_8

    Chapter  Google Scholar 

  44. Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 566–580. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_53

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CEA, LIST, Software Reliability Laboratory, PC 174, 91191, Gif-sur-yvette, France

    Nikolai Kosmatov & Julien Signoles

  2. Inria, Université Paris-Saclay, 91893, Palaiseau, France

    Claude Marché

  3. LRI, CNRS and University of Paris-Sud, 91405, Orsay, France

    Claude Marché

  4. AdaCore, 75009, Paris, France

    Yannick Moy

Authors
  1. Nikolai Kosmatov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Claude Marché
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yannick Moy
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Julien Signoles
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Claude Marché .

Editor information

Editors and Affiliations

  1. Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Kosmatov, N., Marché, C., Moy, Y., Signoles, J. (2016). Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science(), vol 9952. Springer, Cham. https://doi.org/10.1007/978-3-319-47166-2_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47166-2_32

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47165-5

  • Online ISBN: 978-3-319-47166-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation