Abstract
Using tools for deductive verification, such as Frama-C, typically imposes substantial work overhead in the form of manually writing annotations. In this chapter, we investigate techniques for alleviating this problem by means of automatic inference of ACSL specifications. To this end, we present the Frama-C plugin Saida, which uses the assertion-based model checker TriCera as a back-end tool for inference of function contracts. TriCera transforms the program, and specifications provided as assume and assert statements, into a set of constrained Horn clauses (CHC), and relies on CHC solvers for the verification of these clauses. Our approach assumes that a C program consists of one entry-point (main) function and a number of helper functions, which are called from the main function either directly or transitively. Saida takes as input such a C program, where the main function is annotated with an ACSL function contract, and translates the contract into a harness function, comprised mainly of assume and assert statements. The harness function, together with the original program, is used as input for TriCera and, from the output of the CHC solver, TriCera infers pre- and post-conditions for all the helper functions in the C program, and translates them into ACSL function contracts. We illustrate on several examples how Saida can be used in practice, and discuss ongoing work on extending and improving the plugin.
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
Notes
- 1.
Note that the pre-condition true can be omitted since it is the default pre-condition of ACSL function contracts. We include it here for clarity.
- 2.
Note that we consider assert as a statement, so that it differs from the assert macro described in the C99 standard.
- 3.
It should be noted here that reading from an indeterminate variable might be undefined behavior (if the value is a trap representation). However, since the harness function will only be used as input to TriCera, and not executed as a C program, we are not overly concerned about undefined behaviors here.
- 4.
References
Ahrendt W, Beckert B, Bubel R, Hähnle R, Schmitt PH, Ulbrich M (eds) (2016) Deductive software verification-the key book-from theory to practice. Lecture notes in computer science, vol 10001. Springer. https://doi.org/10.1007/978-3-319-49812-6
Albarghouthi A, Dillig I, Gurfinkel A (2016) Maximal specification synthesis. In: Annual symposium on principles of programming languages (POPL). https://doi.org/10.1145/2837614.2837628
Alshnakat A, Gurov D, Lidström C, Rümmer P (2020) Constraint-based contract inference for deductive verification. Springer International Publishing. https://doi.org/10.1007/978-3-030-64354-6_6
Amilon J (2021) Automated inference of ACSL function contracts using TriCera. Master’s thesis, KTH, School of Electrical Engineering and Computer Science (EECS)
Baudin P, Bobot F, Correnson L, Dargaye Z, Blanchard A WP Plug-in Manual–Frama-C 23.1 (Vanadium). CEA LIST. https://frama-c.com/download/frama-c-wp-manual.pdf
Baudin P, Filliâtre JC, Marché C, Monate B, Moy Y, Prevosto V ACSL: ANSI/ISO C specification language. http://frama-c.com/acsl.html
Beckert B, Kirsten M, Klamroth J, Ulbrich M (2020) Modular verification of JML contracts using bounded model checking. In: Int. Symp. On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)
Bjørner N, Gurfinkel A, McMillan KL, Rybalchenko A (2015) Horn clause solvers for program verification. In: Beklemishev LD, Blass A, Dershowitz N, Finkbeiner B, Schulte W (eds) Fields of logic and computation II-essays dedicated to Yuri Gurevich on the occasion of His 75th birthday. Lecture notes in computer science. vol 9300. Springer. https://doi.org/10.1007/978-3-319-23534-9_2
Bjørner N, McMillan KL, Rybalchenko A (2013) On solving universally quantified horn clauses. In: Logozzo F, Fähndrich M (eds) International symposium on static analysis (SAS). Lecture notes in computer science, vol 7935. Springer. https://doi.org/10.1007/978-3-642-38856-9_8
Blazy S, Bühler D, Yakobowski B (2017) Structuring abstract interpreters through state and value abstractions. In: 18th international conference on verification model checking and abstract interpretation (VMCAI 2017). Proceedings of the international conference on verification model checking and abstract interpretation. LNCS, vol 10145. Paris, France, pp 112–130. https://doi.org/10.1007/978-3-319-52234-0_7. https://hal-cea.archives-ouvertes.fr/cea-01808886
Clarke EM, Henzinger TA, Veith H, Bloem R (eds) (2018) Handbook of model checking. Springer. https://doi.org/10.1007/978-3-319-10575-8
Cousot P (2012) Formal verification by abstract interpretation. In: Goodloe A, Person S (eds) 4th NASA formal methods symposium (NFM 2012). Lecture notes in computer science, vol 7226. Springer-Verlag, Heidelberg, pp 3–7. https://doi.org/10.1007/978-3-642-28891-3_3
Cuoq P, Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2012) Frama-C: a software analysis perspective. In: International conference on software engineering and formal methods (SEFM). https://doi.org/10.1007/s00165-014-0326-7
Denney E, Fischer B (2006) A generic annotation inference algorithm for the safety certification of automatically generated code. In: International conference on generative programming and component engineering (GPCE). https://doi.org/10.1145/1173706.1173725
Dijkstra EW (1975) Guarded commands, nondeterminacy and formal derivation of programs. Commun ACM 18(8):453–457. https://doi.org/10.1145/360933.360975
Dijkstra EW (1976) A discipline of programming. Prentice-Hall. http://www.worldcat.org/oclc/01958445
Esen Z, Rümmer P (2022) An SMT-LIB theory of heaps. In: Déharbe D, Hyvärinen AEJ (eds) International workshop on satisfiability modulo theories (SMT), vol 3185, pp 38–53. http://ceur-ws.org/Vol-3185/paper1180.pdf
Esen Z, Rümmer P (2022) TriCera: verifying C programs using the theory of heaps. In: Annual conference on formal methods in computer aided design (FMCAD)
Flanagan C, Saxe J (2001) Avoiding exponential explosion: generating compact verification conditions. In: Annual ACM symposium on principles of programming languages (POPL), vol 36. https://doi.org/10.1145/373243.360220
Floyd RW (1967) Assigning meanings to programs. In: Symposium on applied mathematics, vol 19. http://laser.cs.umass.edu/courses/cs521-621.Spr06/papers/Floyd.pdf
Gordon M, Collavizza H (2010) Forward with hoare. In: Reflections on the Work of CAR Hoare. Springer, pp 101–121. https://doi.org/10.1007/978-1-84882-912-1_5
Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: International conference on programming language design and implementation (PLDI). https://doi.org/10.1145/2254064.2254112
Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10). https://doi.org/10.1145/363235.363259
Hojjat H, Rümmer P (2018) The ELDARICA horn solver. In: Bjørner N, Gurfinkel A (eds) Annual conference on formal methods in computer aided design (FMCAD). https://doi.org/10.23919/FMCAD.2018.8603013
Hojjat H, Rümmer P, Subotic P, Yi W (2014) Horn clauses for communicating timed systems. In: Workshop on horn clauses for verification and synthesis (HCVS). https://doi.org/10.4204/EPTCS.169.6
Horn A (1951) On sentences which are true of direct unions of algebras. J Symb Log 16(1). https://doi.org/10.2307/2268661
International organization for standardization (ISO) The ANSI C standard (C99). http://www.open-std.org/JTC1/SC22/WG14/www/docs/n1124.pdf
Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2015) Frama-C: a software analysis perspective. Form Asp Comput. https://doi.org/10.1007/s00165-014-0326-7
Komuravelli A, Gurfinkel A, Chaki S, Clarke EM (2013) Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina N, Veith H (eds) International conference on computer aided verification (CAV). Lecture notes in computer science, vol 8044. Springer. https://doi.org/10.1007/978-3-642-39799-8_59
McCarthy J (1962) Towards a mathematical science of computation. In: Congress on information processing. North-Holland. https://dblp.org/rec/conf/ifip/McCarthy62.bib
Moy Y (2008) Sufficient preconditions for modular assertion checking. In: International conference on verification, model checking, and abstract interpretation (VMCAI). https://doi.org/10.1007/978-3-540-78163-9_18
Nielson HR, Nielson F (2007) Semantics with applications: an appetizer. Springer-Verlag. https://doi.org/10.1007/978-1-84628-692-6
Nyberg M, Gurov D, Lidström C, Rasmusson A, Westman J (2018) Formal verification in automotive industry: enablers and obstacles. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation. Industrial practice. Springer International Publishing
Seghir MN, Kroening D (2013) Counterexample-guided precondition inference. In: European symposium on programming languages and systems (ESOP). https://doi.org/10.1007/978-3-642-37036-6_25
Seghir MN, Schrammel P (2014) Necessary and sufficient preconditions via eager abstraction. In: Asian symposium on programming languages and systems (APLAS). https://doi.org/10.1007/978-3-319-12736-1_13
Singleton JL, Leavens GT, Rajan H, Cok DR (2019) Inferring concise specifications of APIs. CoRR. http://arxiv.org/abs/1905.06847
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Amilon, J., Esen, Z., Gurov, D., Lidström, C., Rümmer, P. (2024). An Exercise in Mind Reading: Automatic Contract Inference for Frama-C. 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_13
Download citation
DOI: https://doi.org/10.1007/978-3-031-55608-1_13
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)