This page is dedicated to publications related to Frama-C. They are categorized by plug-ins. Manuals appear first, then founding thesis and articles and finally an inexhaustive lists of other relevant articles. Each category is sorted by inverse order of date of publication.
Please feel free to update this page with your own knowledge. Add links when possible and only if they do respect copyright.
Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy and Virgile Prevosto.
ACSL: ANSI/ISO C Specification Language. Version 1.6
The reference manual of ACSL, the specification language used by Frama-C.
Jochen Burghardt, Jens Gerlach, Kerstin Hartig, Hans Pohl and Juan Soto.
ACSL by Example. A fairly complete tour of ACSL features through various functions inspired from C++ STL.
Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles and Boris Yakobowski.
Frama-C, A Software Analysis Perspective.
In proceedings of International Conference on Software Engineering and Formal Methods 2012 (SEFM'12), October 2012.
This paper presents a synthetic view of Frama-C, its main and composite analyses, and some of its industrial achievements.
Loïc Correnson and Julien Signoles.
Combining Analyses for C Program Verification.
In proceedings of International Workshop on Formal Methods for Industrial Critical Systems 2012 (FMICS'12), August 2012.
This paper explains how Frama-C combines several partial results coming from its plug-ins into a fully consolidated validity status for each program property.
Une bibliothèque de typage dynamique en OCaml.
In Hermann, editor, JFLA 11, Actes des Journées Francophones des Langages Applicatifs 2011, January 2011. In French.
Cet article présente une bibliothèque OCaml fournissant une représentation dynamique des types monomorphes, y compris pour les instances des types polymorphes et les types de données abstraits. Elle permet ainsi de voir les types OCaml comme des citoyens de première classe. Elle comble aussi le fossé séparant OCaml des langages dynamiques en mêlant vérifications statiques et dynamiques des types. Nous nous concentrons ici sur le coeur de son implantation, ses propriétés théoriques et l'usage qui en est fait dans
Frama-C, plateforme logicielle libre d'analyse statique de programmes C au sein de laquelle cette bibliothèque est distribuée.
Pascal Cuoq and Julien Signoles.
Experience Report: OCaml for an Industrial-Strength Static Analysis Framework.
In Proceedings of International Conference of Functional Programming (ICFP'09), pages 281–286, September 2009.
This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use
of resources…) but could have prevented the use of OCaml for this project if they had been missing.
Foncteurs impératifs et composés: la notion de projets dans Frama-C.
In Hermann, editor, JFLA 09, Actes des vingtièmes Journées Francophones des Langages Applicatifs 2009, volume 7.2 of Studia Informatica Universalis, pages 245–280, June 2009. In French.
Cet article présente la bibliothèque de projets de Frama-C, une plateforme facilitant le développement d'analyseurs statiques de programmes C. Grâce à sa description, nous présentons une utilisation originale des foncteurs du système de modules de ML qui exploite aussi bien leur caractère impératif que compositionnel. Ceci est le seul véritable recours pour réaliser la fonctionalité souhaitée de manière bien typée. En outre, nous montrons un exemple peu fréquent d'un même foncteur appliqué plusieurs centaines de fois. Cet article introduit aussi la plateforme Frama-C elle-même, à travers un de ses aspects essentiels, la notion de projet.
Dillon Pariente and Emmanuel Ledinot.
Formal Verification of Industrial C Code using Frama-C: a Case Study.
In Proceedings of First International Conference on Formal Verification of Object-Oriented Software (FoVeOOS'10), June 2010.
This paper gives some results and lessons learnt with Frama-C, a static analysis toolbox, used to prove behavioral and safety properties on an industrial code. After a short presentation of the methods and tools background, the related industrial use case is briefly exposed, with an overview of the process that was followed. Then the positive results obtained so far are presented, with a few practices and additional tools developed in-house. To conclude, this paper presents some needs and future work directions that should
be addressed, to ensure a technology readiness level compliant with operational use of formal verification into an industrial development environment.
See also the associated video
Matti Mantere, Ilkka Uusitalo, Juha Röning.
Comparison of Static Code Analysis Tools.
securware, Third International Conference on Emerging Security Information, Systems and Technologies, pages 15–22, June 2009.
In this paper we compare three static code analysis tools. The tools represent three different approaches in the field of static analysis: Fortify SCA is a non-annotation based heuristic analyzer, Splint represents an annotation based heuristic analyzer, and Frama-C an annotation based correct analyzer. The tools are compared by analysing their performance when checking a demonstration code with intentionally implemented errors.
Géraud Canet, Pascal Cuoq and Benjamin Monate.
A Value Analysis for C Programs.
In Proceedings of the Ninth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM'09). September 2009.
We demonstrate the value analysis of Frama-C. Frama-C is an Open Source static analysis framework for the C language. In Frama-C, each static analysis technique, approach or idea can be implemented as a new plug-in, with the opportunity to obtain information from other plug-ins, and to leave the verification of difficult properties to yet other plug-ins. The new analysis may in turn provide access to the data it has computed. The value analysis of Frama-C is a plug-in based on abstract interpretation. It computes and stores supersets of possible values for all the variables at each statement of the analyzed program. It handles pointers, arrays, structs, and heterogeneous pointer casts. Besides producing supersets of possible values for the variables at each point of the execution, the value analysis produces run-time-error alarms. An alarm is emitted for each operation in the analyzed program where the value analysis cannot guarantee that there will not be a run-time error.
Pascal Cuoq and Damien Doligez.
Hashconsing in an incrementally garbage-collected system: a story of weak pointers and hashconsing in OCaml 3.10.2.
In Proceedings of the 2008 ACM SIGPLAN Workshop on ML (ML'08), pages 13–22, September 2008.
This article describes the implementations of weak pointers, weak hashtables and hashconsing in version 3.10.2 of the Objective Caml system, with focus on several performance pitfalls and their solutions.
Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr, Boris Yakobowski and Xuejun Yang.
Testing Static Analyzers with Randomly Generated Programs.
In Proceedings of the 4th NASA Formal Methods Symposium (NFM 2012), LNCS 7226, April 2012.
Chatzieleftheriou, G. and Katsaros, P.
Test driving static analysis tools in search of C code vulnerabilities.
In Proceedings of the 6th IEEE International Workshop on Security, Trust, and Privacy for Software Applications (STPSA'11), Munich, Germany, IEEE Computer Society, 2011.
Static Analysis of the XEN Kernel using Frama-C.
Journal of Universal Computer Science, volume 16, issue 4, 2010.
In this paper, we describe the static analysis of the XEN 3.0.3 hypervisor using the Frama-C static analysis tool.
Pascal Berthomé, Karinne Heydemann, Xavier Kauffmann-Tourkestansky and Jean-François Lalande.
Attack model for verification of interval security properties for smart card C codes.
Proceedings of the 5th Workshop on Programming Languages and Analysis for Security (PLAS'10). 2010.
Smart card programs are subject to physical attacks that disturb the execution of the embedded code. These attacks enable attackers to steal valuable information or to force a malicious behavior upon the attacked code. This paper proposes a methodology to check interval security properties on smart card source codes. The goal is to identify critical attacks that violate these security properties. The verification takes place at source-level and considers all possible attacks thanks to a proposed source-level model of physical attacks. The paper defines an equivalence relation between attacks and shows that a code can be divided into areas where attacks are equivalent. Thus, verifying an interval security property considering all the possible attacks requires to verify as many codes as the number of equivalence classes. This paper provides a reduction algorithm to define the classes i.e. the minimal number of attacked codes that covers all possible attacks. The paper also proposes a solution to make the property verification possible for large codes or codes having unknown source parts.
Pascal Cuoq, Benjamin Monate, Anne Pacalet and Virgile Prevosto.
Functional Dependencies of C Functions via Weakest Pre-Conditions
International Journal on Software Tools for Technology Transfer (STTT), edition VSTTE 2009-2010, SpringerLink
Sufficient Preconditions for Modular Assertion Checking.
In Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'08). January 2008.
Assertion checking is the restriction of program verification to validity of program assertions. It encompasses safety checking, which is program verification of safety properties, like memory safety or absence of overflows. In this paper, we consider assertion checking of program parts instead of whole programs, which we call modular assertion checking. Classically, modular assertion checking is possible only if the context in which a program part is executed is known. By default, the worst-case context must be assumed, which may impair the verification task. It usually takes user effort to detail enough the execution context for the verification task to succeed, by providing strong enough preconditions. We propose a method to automatically infer sufficient preconditions in the context of modular assertion checking of imperative pointer programs. It combines abstract interpretation, weakest precondition calculus and quantifier elimination. We instantiate this method to prove memory safety for C and Java programs, under some memory separation conditions.
Checking C Pointer Programs for Memory Safety.
INRIA Research Report n°6334, October 2007.
We propose an original approach for checking memory safety of C pointer programs that do not include casts, structures, double indirection and memory deallocation. This involves first identifying aliasing and strings, which we do in a local setting rather than through a global analysis as it is done usually. Our separation analysis in particular is a totally new treatment of non-aliasing. We present for the first time two abstract lattices to deal with local pointer aliasing and local pointer non-aliasing in an abstract interpretation framework. The key feature of our work is to combine abstract interpretation techniques and deductive verification. The approach is modular and contextual, thanks to the use of Hoare-style annotations (pre- and postconditions), allowing to verify each C function independently. Abstract interpretation techniques are used to automatically generate such annotations, in an idiomatic way: standard practice of C programming is identified and incorporated as heuristics. Abstract interpretation and deductive verification are both used to check these annotations in a sound way. Our first contribution is the design of an abstract domain for implications, which makes it possible to build efficient contextual analyses. Our second contribution is an efficient back-and-forth propagation method to generate contextual annotations in a modular way, in the framework of abstract interpretation. It considers the safety conditions to prove as a starting point, which focuses the analysis on the paths of interest. Thanks to previously unknown loop refinement operators, this propagation method does not require iterating around loops. We implemented our method in Caduceus, a tool for the verification of C programs, and successfully verified automatically the C standard string library functions.
Union and Cast in Deductive Verification.
In Proceedings of the C/C++ Verification Workshop (CCV'07), July 2007.
Deductive verification based on weakest-precondition calculus has proved effective at proving imperative programs, through a suitable encoding of memory as functional arrays (a.k.a. the Burstall-Bornat model). Unfortunately, this encoding of memory makes it impossible to support features like union and cast in C. We show that an interesting subset of those unions and casts can be encoded as structure subtyping, on which it is possible to extend the Burstall- Bornat encoding. We present an automatic translation from C to an intermediate language Jessie on which this extended interpretation is performed.
Yannick Moy and Claude Marché.
Inferring local (non-)aliasing and strings for memory safety.
In Proceedings of Heap Analysis and Verification (HAV’07), Braga, Portugal, March 2007.
We propose an original approach for checking memory safety of C pointer programs, by combining deductive verification and abstract interpretation techniques. The approach is modular and contextual, thanks to the use of Hoare-style annotations (pre- and postconditions), allowing us to verify each C function independently. Deductive verification is used to check these annotations in a sound way. Abstract interpretation techniques are used to automatically generate such annotations, in an idiomatic way: standard practice of C programming is identified and incorporated as heuristics. Our first contribution is a set of techniques for identifying aliasing and strings, which we do in a local setting rather than through a global analysis as it is done usually. Our separation analysis in particular is a totally new treatment of non-aliasing. We present for the first time two abstract lattices to deal with local pointer aliasing and local pointer non-aliasing in an abstract interpretation framework. Our second contribution is the design of an abstract domain for implications, which makes it possible to build efficient contextual analyses. Our last contribution is an efficient back-and-forth propagation method to generate contextual annotations in a modular way, in the framework of abstract interpretation. We implemented our method in Caduceus, a tool for the verification of C programs, and successfully generated appropriate annotations for the C standard string library functions.
Thierry Hubert and Claude Marché.
Separation analysis for deductive verification.
In Heap Analysis and Verification (HAV'07), pages 81-93, Braga, Portugal, March 2007.
Jochen Burghardt, Jens Gerlach, Hans Pohl and Juan Soto.
An Experience Report on the Verification of Algorithms in the C++ Standard Library using Frama-C.
In First Proceedings of International Conference of Formal Verification of Object-Oriented Software (FoVeOOS'10), June 2010.
Over the past few years, we have been conducting assessment studies to determine the utility of the Frama-C/Jessie platform of software analyzers (in conjunction with automatic theorem provers) for the formal verification of software. In this experience report, we discuss experiments in the verification of algorithms in the C++ Standard Library based on tool-supported Hoare-style weakest precondition computations to formally prove ACSL (ANSI/ISO C Specification Language) properties. Often automated provers are unable to perform inductive proofs. Hence, we introduce an approach to guide automated provers to find an inductive proof using auxiliary C-code corresponding to the proof structure. We also present a method to verify that a function only permutes the contents of an array, and obtain the relation between the pre- and post-index for each array element for use in later specification properties. Furthermore, we describe an approach to prove the essential properties of a function independent of each other, supplying for each task only
the assumptions actually needed, i.e., related to the current goal. This approach reduces the proof search space and leads to higher verification rates for automatic provers. However, additional methods and tool support are desired to overcome drawbacks from a software engineering point of view. Finally, we sketch some ideas for an extension of ACSL for C++.
Stéphane Duprat, Pierre Gaufillet, Victoria Moya Lamiel and Frédéric Passarello.
Formal verification of SAM state machine implementation.
In Proceedings of Embedded Real Time Software and Systems (ERTS²'10), May 2010.
This paper reports the results of an experiment about the formal verification of source code made according to an EMF model. Models define the semantics of a system whereas the source code defines its implementation. We applied
this solution to a model of Automaton in SAM language and its C language implementation. The technical environment is close to an industrial operational context and all the tools are available.
The experimentation has succeeded and has to be consolidated with bigger cases before an introduction in the operational development process. More generally, this solution must be extended to
other model languages.
Benjamin Monate and Julien Signoles.
Slicing for Security of Code.
In Proceedings of the 1st international conference on Trusted Computing and Trust in Information Technologies (TRUST'08), pages 133–142, March 2008.
Bugs in programs implementing security features can be catastrophic: for example they may be exploited by malign users to gain access to sensitive data. These exploits break the confidentiality of information. All security analyses assume that softwares implementing security features correctly implement the security policy, i.e. are security bug-free. This assumption is almost always wrong and IT security administrators consider that any software that has no security patches on a regular basis should be replaced as soon as possible. As programs implementing security features are usually large, manual auditing is very error prone and testing techniques are very expensive. This article proposes to reduce the code that has to be audited by applying a program reduction technique called slicing. Slicing transforms a source code into an equivalent one according to a set of criteria. We show that existing slicing criteria do not preserve the confidentiality of information. We introduce a new automatic and correct source-to-source method properly preserving the confidentiality of information i.e. confidentiality is guaranteed to be exactly the same in the original program and in the sliced program.
Nicky Williams, Bruno Marre, Patricia Mouy and Muriel Roger.
PathCrawler: automatic generation of path tests by combining static and dynamic analysis.
In Proc. 5th European Dependable Computing Conference (EDCC-5), Budapest, Hungary, April 20-22, 2005, Lecture Notes in Computer Science 3463 Springer 2005, ISBN 3-540-25723-3, Budapest, Hungary, April 2005, pages 281-292.
The final publication is available at www.springerlink.com
Patricia Mouy, Bruno Marre, Nicky Williams and Pascale Le Gall.
Generation of all-paths unit test with function calls.
In Proc. 1st Intl. Conference on Software Testing, Verification, and Validation, ICST 2008, Lillehammer, Norway, April 9-11, 2008, IEEE Computer Society, 2008, pages 32-41.
The final publication is available from IEEE. http://doi.ieeecomputersociety.org/10.1109/ICST.2008.35
Bernard Botella, Mickaël Delahaye, Stéphane Hong-Tuan-Ha, Nikolai Kosmatov, Patricia Mouy, Muriel Roger and Nicky Williams.
Automating Structural Testing of C Programs: Experience with PathCrawler.
In Proc. 4th Intl. Workshop on Automation of Software Test, AST 2009, Vancouver, BC, Canada, May 18-19, 2009, IEEE Computer Society 2009, pages 70-78.
The final publication is available from IEEE. http://dx.doi.org/10.1109/IWAST.2009.5069043
Abstract path testing with PathCrawler.
©ACM, 2010. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proc. 5th Workshop on Automation of Software Test (AST'10), Cape Town, South Africa, May 2-8 2010, ACM New York, NY, USA, 2010, ISBN 978-1-60558-970-1, pages 35-42. http://doi.acm.org/10.1145/1808266.1808272
Nikolai Kosmatov, Bernard Botella, Muriel Roger and Nicky Williams.
Online Test Generation with PathCrawler. Tool demo.
Best demo award.
In Proc. of the 3rd International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2011), Berlin, Germany, March 2011, IEEE Computer Society Press, 2011, ISBN 978-1-4577-0019-4, pages 316-317.
The final publication is available from IEEE. http://dx.doi.org/10.1109/ICSTW.2011.85
Nicky Williams and Nikolai Kosmatov.
Structural Testing with PathCrawler. Tutorial Synopsis.
In Proc. 12th International Conference on Quality Software (QSIC 2012), Xi'an, China, August 27-29, 2012, IEEE Computer Society, 2012, ISBN 978-0-7695-4833-3, pages 289-292.
The final publication will be available from IEEE. http://www.ieee.org
Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro.
A Lesson on Structural Testing with PathCrawler-online.com.
In Proc. Tests and Proofs - 6th International Conference, TAP 2012, Prague, Czech Republic, May 31 - June 1, 2012, Springer, Lecture Notes in Computer Science, vol. 7305, 2012, ISBN 978-3-642-30472-9, pages 169-175.
The final publication is available at www.springerlink.com
These publications are related to Frama-C plug-ins which are not available from the official Frama-C website (http://frama-c.com). These plug-ins may be either closed or open source.
Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas.
Certifying and reasoning on cost annotations in C programs.
In Proceedings of the 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2012), Paris, France, August 2012.
We present a so-called labelling method to enrich a compiler in order to turn it into a “cost annotating compiler”, that is, a compiler which can lift pieces of information on the execution cost of the object code as cost annotations on the source code. These cost annotations characterize the execution costs of code fragments of constant complexity. … we present a Frama-C plugin that uses our cost annotating compiler to automatically infer trustworthy logic assertions about the concrete worst case execution cost of programs written in a fragment of the C language. … We report our experimentations on some C programs, especially programs generated by a compiler for the synchronous programming language Lustre used in critical embedded software.
Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya Lamiel.
Fan-C, a Frama-C plug-in for data flow verification.
In Proceedings of Embedded Real Time Software and Systems (ERTS'12).
Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques Julliand.
The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging.
In Proceedings of the 5th International Conference on Tests & Proofs (TAP 2011), Zurich, Switzerland, June 2011.
This short paper presents a prototype tool called SANTE (Static ANalysis and TEsting) implementing an original method combining value analysis, program slicing and structural test generation for verification of C programs.
First, value analysis is called to generate alarms when it can not guarantee the absence of errors. Then the program is reduced by program slicing. Alarm-guided test generation is then used to analyze the simplified program(s) in order to confirm or reject alarms.
Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques Julliand.
Combining static analysis and test generation for C program debugging.
In Proceedings of the 4th International Conference on Tests & Proofs (TAP 2010), pages 94-100, Malaga, Spain, July 2010.
This paper presents our ongoing work on a tool prototype called SANTE (StaticANalysis and TEsting), implementing a combination of static analysis
and structural program testing for detection of run-time errors in C programs. First, a static analysis tool (Frama-C) is called to generate alarms when it cannot ensure the absence of run-time errors. Second, these alarms guide a structural test generation tool (PathCrawler) trying to confirm alarms by activating bugs on sometest cases.Our experiments on real-life software showthat
this combination can outperform the use of each technique independently.
Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques Julliand.
Program slicing enhances a verification technique combining static and dynamic analysis.
In Proceedings of the 27th Symposium On Applied Computing (SAC 2012), pages 1284-1291, Trento, Italy, March 2012.
Recent research proposed efficient methods for software verification combining static and dynamic analysis, where static analysis reports possible runtime errors (some of which may be false alarms) and test generation confirms or rejects them. However, test generation may time out on real-sized programs before confirming some alarms as real bugs or rejecting some others as unreachable. To overcome this problem, we propose to reduce the source code by program slicing before test generation. This paper presents new optimized and adaptive usages of program slicing, provides underlying theoretical results and the algorithm these usages rely on. The method is implemented in a tool prototype called sante (Static ANalysis and TEsting). Our experiments show that our method with program slicing outperforms previous combinations of static and dynamic analysis. Moreover, simplifying the program makes it easier to analyze detected errors and remaining alarms. To appear.
Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel.
SIDAN: a tool dedicated to Software Instrumentation for Detecting Attacks on Non-control-data.
4th International Conference on Risks and Security of Internet and Systems (CRISIS'2009), October 2009.
Dumitru Ceara, Laurent Mounier and Marie-Laure Potet.
Taint Dependency Sequences: a characterization of insecure execution paths based on input-sensitive cause sequences.
Modeling and Detecting Vulnerabilities workshop (MDV'10), associated to ICST 2010, April 2010.
David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien Signoles.
Taster, a Frama-C plug-in to enforce Coding Standards.
In Proceedings of Embedded Real Time Software and Systems (ERTS'10), May 2010.
Enforcing Coding Standards is part of the traditional concerns of industrial software developments. In this paper, we present a framework based on the open source Frama-C platform for easily developing syntactic, typing (and even some semantic) analyses of C source code, among which conformance to Coding Standards. We report on our successful attempt to develop a Frama-C plug-in named Taster, in order to replace a commercial, off-the-shelf, legacy tool in the verification process of several Airbus avionics software products. We therefore present the types of coding rules to be verified, the Frama-C platform and the Taster plug-in. We also discuss ongoing industrial deployment and qualification activities.