Abstract
Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.
This work was partly supported by ANR U3CAT and Veridyc, and FUI9 Hi-Lite projects.
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
Preview
Unable to display preview. Download preview PDF.
References
Bardin, S., Herrmann, P.: OSMOSE: automatic structural testing of executables. Software Testing, Verification and Reliability 21(1), 29–54 (2011)
Bardin, S., Herrmann, P., Védrine, F.: Refinement-Based CFG Reconstruction from Unstructured Programs. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 54–69. Springer, Heidelberg (2011)
Baudin, P., et al.: ACSL: ANSI/ISO C Specification Language Preliminary design, version 1.5 (2010), http://frama-c.com/downloads/acsl_1.5.pdf
Beckman, N., et al.: Proofs from tests. IEEE Trans. Software Eng. 36(4), 495–508 (2010)
Berthomé, P., et al.: Attack model for verification of interval security properties for smart card c codes. In: PLAS, pp. 2:1–2:12. ACM (2010)
Bornat, R.: Proving Pointer Programs in Hoare Logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000)
Botella, B., et al.: Automating structural testing of C programs: Experience with PathCrawler. In: AST, pp. 70–78 (2009)
Bouajjani, A., et al.: On inter-procedural analysis of programs with lists and data. In: PLDI, pp. 578–589 (2011)
Burdy, L., et al.: An overview of JML tools and applications. Software Tools for Technology Transfer 7(3), 212–232 (2005)
Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence 7, 23–50 (1972)
Ceara, D., Mounier, L., Potet, M.-L.: Taint dependency sequences: A characterization of insecure execution paths based on input-sensitive cause sequences. In: ICSTW, Washington, DC, USA, pp. 371–380 (2010)
Chatzieleftheriou, G., Katsaros, P.: Test-driving static analysis tools in search of C code vulnerabilities. In: COMPSAC Workshops, pp. 96–103. IEEE (2011)
Chebaro, O., et al.: Program slicing enhances a verification technique combining static and dynamic analysis. In: SAC (to appear, 2012)
Conchon, S., et al.: The Alt-Ergo Automated Theorem Prover, http://alt-ergo.lri.fr
Coq Development Team. The Coq Proof Assistant Reference Manual, v8.3 edition (2011), http://coq.inria.fr/
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)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTREÉ Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Cuoq, P., et al.: Experience report: OCaml for an industrial-strength static analysis framework. In: ICFP, pp. 281–286. ACM (2009)
Delmas, D., et al.: Taster, a Frama-C plug-in to encode Coding Standards. In: ERTSS (May 2010)
Delmas, D., et al.: Fan-C, a Frama-C plug-in for data flow verification. In: ERTSS (2012)
Demange, D., Jensen, T., Pichardie, D.: A Provably Correct Stackless Intermediate Representation for Java Bytecode. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 97–113. Springer, Heidelberg (2010)
Demay, J.-C., Totel, E., Tronel, F.: Sidan: A tool dedicated to software instrumentation for detecting attacks on non-control-data. In: CRiSIS (October 2009)
Dijkstra, E.W.: A constructive approach to program correctness. BIT Numerical Mathematics. Springer (1968)
Dahlweid, M., et al.: VCC: Contract-based modular verification of concurrent C. In: ICSE Companion. IEEE (2009)
Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319–349 (1987)
Filliâtre, J.-C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Université Paris Sud (March 2003)
Floyd, R.W.: Assigning meanings to programs. Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19 (1967)
Gastin, P., Oddoux, D.: Fast LTL to Büchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Granger, P.: Static Analysis of Linear Congruence Equalities Among Variables of a Program. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493, pp. 169–192. Springer, Heidelberg (1991)
Groslambert, J., Stouls, N.: Vérification de propriétés LTL sur des programmes C par génération d’annotations. In: AFADL (2009) (in French)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACMÂ 12(10) (1969)
Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. PLDI, SIGPLAN Notices 23(7), 35–46 (1988)
IEEE Std 754-2008. IEEE standard for floating-point arithmetic. Technical report (2008), http://dx.doi.org/10.1109/IEEESTD.2008.4610935
ISO/IEC JTC1/SC22/WG14. 9899:TC3: Programming Languages—C (2007), http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf
Kosmatov, N.: Online version of PathCrawler, http://pathcrawler-online.com/
Kosmatov, N.: XI: Constraint-Based Techniques for Software Testing. In: Artificial Intelligence Applications for Improved Software Engineering Development: New Prospects, IGI Global (2010)
Leino, K.R.M.: This is Boogie 2. Microsoft Research (2008)
Marché, C., Moy, Y.: The Jessie plugin for Deduction Verification in Frama-C, version 2.30. INRIA (2012), http://krakatoa.lri.fr/jessie.pdf
Marre, B., Arnould, A.: Test sequences generation from Lustre descriptions: GATeL. In: ASE, Grenoble, France, pp. 229–237 (September 2000)
MathWorks. Polyspace, http://www.mathworks.com/products/polyspace
Meyer, B.: Object-oriented Software Construction. Prentice-Hall (1997)
Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: CC 2002. LNCS, vol. 2304, p. 213. Springer, Heidelberg (2002)
Pariente, D., Ledinot, E.: Formal Verification of Industrial C Code using Frama-C: a Case Study. In: FoVeOOS (2010)
Pnueli, A.: The temporal logic of programs. In: FOCS. IEEE (1977)
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)
Schimpf, J., Shen, K.: ECLiPSe - from LP to CLP. Theory and Practice of Logic Programming 12(1-2), 127–156 (2011)
Signoles, J.: Foncteurs impératifs et composés: la notion de projet dans Frama-C. In: JFLA, Studia Informatica Universalis, vol. 7(2) (2009) (in French)
Signoles, J., Correnson, L., Prevosto, V.: Frama-C Plug-in Development Guide (October 2011), http://frama-c.com/download/plugin-developer.pdf
Stouls, N., Prevosto, V.: Aoraà plug-in tutorial, version Nitrogen-20111001 (October 2011), http://frama-c.com/download/frama-c-aorai-manual.pdf
Williams, N., Marre, B., Mouy, P., Roger, M.: PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis. In: Dal Cin, M., Kaâniche, M., Pataricza, A. (eds.) EDCC 2005. LNCS, vol. 3463, pp. 281–292. Springer, Heidelberg (2005)
Yakobowski, B., et al.: Formal verification of software important to safety using the Frama-C tool suite. In: NPIC (July 2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B. (2012). Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds) Software Engineering and Formal Methods. SEFM 2012. Lecture Notes in Computer Science, vol 7504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33826-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-33826-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33825-0
Online ISBN: 978-3-642-33826-7
eBook Packages: Computer ScienceComputer Science (R0)