Frama-C

Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C. Frama-C gathers several static analysis techniques in a single collaborative framework. The collaborative approach of Frama-C allows static analyzers to build upon the results already computed by other analyzers in the framework. Thanks to this approach, Frama-C provides sophisticated tools, such as a slicer and dependency analysis.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 19 articles )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Monniaux, David: A survey of satisfiability modulo theory (2016)
  2. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  3. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  4. Methni, Amira; Lemerre, Matthieu; Ben Hedia, Belgacem; Haddad, Serge; Barkaoui, Kamel: Specifying and verifying concurrent C programs with TLA+ (2015) ioport
  5. David R. Cok: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse (2014) arXiv
  6. Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
  7. Kahl, Wolfram: Towards “mouldable code” via nested code graph transformation (2014)
  8. Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
  9. Ayache, Nicolas; Amadio, Roberto M.; Régis-Gianas, Yann: Certifying and reasoning on cost annotations in C programs (2012) ioport
  10. Cuoq, Pascal; Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2012) ioport
  11. Greenaway, David; Andronick, June; Klein, Gerwin: Bridging the gap: automatic verified abstraction of C (2012)
  12. Bobot, François; Paskevich, Andrei: Expressing polymorphic types in a many-sorted language (2011)
  13. Chebaro, Omar; Kosmatov, Nikolai; Giorgetti, Alain; Julliand, Jacques: The SANTE tool: value analysis, program slicing and test generation for C program debugging (2011) ioport
  14. Collins, Pieter; Niqui, Milad; Revol, Nathalie: A validated real function calculus (2011)
  15. Frade, Maria João; Pinto, Jorge Sousa: Verification conditions for source-level imperative programs (2011)
  16. Ayad, Ali; Marché, Claude: Multi-prover verification of floating-point programs (2010)
  17. Butelle, Franck; Hivert, Florent; Mayero, Micaela; Toumazet, Frédéric: Formal proof of SCHUR conjugate function (2010)
  18. Nguyen, An N.; Quan, Tho T.; Nguyen, Phung H.; Bui, Thang H.: COMBINE: a tool on combined formal methods for bindingly verification (2010) ioport
  19. Blazy, Sandrine; Leroy, Xavier: Mechanized semantics for the clight subset of the C language (2009)