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 28 articles )

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

1 2 next

  1. Léchenet, Jean-Christophe; Kosmatov, Nikolai; Le Gall, Pascale: Cut branches before looking for bugs: certifiably sound verification on relaxed slices (2018)
  2. Blazy, Sandrine; Bühler, David; Yakobowski, Boris: Structuring abstract interpreters through state and value abstractions (2017)
  3. Botbol, Vincent; Chailloux, Emmanuel; Le Gall, Tristan: Static analysis of communicating processes using symbolic transducers (2017)
  4. Wang, Wei; Barrett, Clark; Wies, Thomas: Partitioned memory models for program analysis (2017)
  5. Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
  6. Monniaux, David: A survey of satisfiability modulo theory (2016)
  7. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  8. Wang, Timothy; Jobredeaux, Romain; Pantel, Marc; Garoche, Pierre-Loic; Feron, Eric; Henrion, Didier: Credible autocoding of convex optimization algorithms (2016)
  9. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  10. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  11. Methni, Amira; Lemerre, Matthieu; Ben Hedia, Belgacem; Haddad, Serge; Barkaoui, Kamel: Specifying and verifying concurrent C programs with TLA+ (2015) ioport
  12. David R. Cok: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse (2014) arXiv
  13. Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
  14. Kahl, Wolfram: Towards “mouldable code” via nested code graph transformation (2014)
  15. Filli^atre, Jean-Christophe: One logic to use them all (2013)
  16. Leino, K. Rustan M.: Automating theorem proving with SMT (2013)
  17. Ayache, Nicolas; Amadio, Roberto M.; Régis-Gianas, Yann: Certifying and reasoning on cost annotations in C programs (2012) ioport
  18. Cuoq, Pascal; Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2012) ioport
  19. Greenaway, David; Andronick, June; Klein, Gerwin: Bridging the gap: automatic verified abstraction of C (2012)
  20. Anureev, I. S.: Integrated approach to analysis and verification of imperative programs (2011)

1 2 next