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

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

1 2 3 next

  1. Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir: Leveraging compiler intermediate representation for multi- and cross-language verification (2020)
  2. Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2020)
  3. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  4. Barany, Gergö: Liveness-driven random program generation (2018)
  5. Davy, Guillaume; Feron, Eric; Garoche, Pierre-Loic; Henrion, Didier: Experiments in verification of linear model predictive control: automatic generation and formal verification of an interior point method algorithm (2018)
  6. Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov: Lemma Functions for Frama-C: C Programs as Proofs (2018) arXiv
  7. Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina: Understanding parameters of deductive verification: an empirical investigation of key (2018)
  8. Léchenet, Jean-Christophe; Kosmatov, Nikolai; Le Gall, Pascale: Cut branches before looking for bugs: certifiably sound verification on relaxed slices (2018)
  9. Müller, Peter (ed.); Schaefer, Ina (ed.): Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018 (2018)
  10. Petiot, Guillaume; Kosmatov, Nikolai; Botella, Bernard; Giorgetti, Alain; Julliand, Jacques: How testing helps to diagnose proof failures (2018)
  11. Roux, Pierre; Iguernlala, Mohamed; Conchon, Sylvain: A non-linear arithmetic procedure for control-command software verification (2018)
  12. Summers, Alexander J.; Müller, Peter: Automating deductive verification for weak-memory programs (2018)
  13. Blazy, Sandrine; Bühler, David; Yakobowski, Boris: Structuring abstract interpreters through state and value abstractions (2017)
  14. Botbol, Vincent; Chailloux, Emmanuel; Le Gall, Tristan: Static analysis of communicating processes using symbolic transducers (2017)
  15. Wang, Wei; Barrett, Clark; Wies, Thomas: Partitioned memory models for program analysis (2017)
  16. Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
  17. Monniaux, David: A survey of satisfiability modulo theory (2016)
  18. Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
  19. Wang, Timothy; Jobredeaux, Romain; Pantel, Marc; Garoche, Pierre-Loic; Feron, Eric; Henrion, Didier: Credible autocoding of convex optimization algorithms (2016)
  20. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)

1 2 3 next