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.


References in zbMATH (referenced in 45 articles )

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

1 2 3 next

  1. Dutle, Aaron; Moscato, Mariano; Titolo, Laura; Muñoz, César; Anderson, Gregory; Bobot, François: Formal analysis of the compact position reporting algorithm (2021)
  2. Francisco Ortin, Javier Escalada: Cnerator: A Python application for the controlled stochastic generation of standard C source code (2021) not zbMATH
  3. Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir: Leveraging compiler intermediate representation for multi- and cross-language verification (2020)
  4. Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2020)
  5. Bouillaguet, Quentin; Bobot, François; Sighireanu, Mihaela; Yakobowski, Boris: Exploiting pointer analysis in memory models for deductive verification (2019)
  6. Barany, Gergö: Liveness-driven random program generation (2018)
  7. 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)
  8. Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov: Lemma Functions for Frama-C: C Programs as Proofs (2018) arXiv
  9. Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina: Understanding parameters of deductive verification: an empirical investigation of key (2018)
  10. Léchenet, Jean-Christophe; Kosmatov, Nikolai; Le Gall, Pascale: Cut branches before looking for bugs: certifiably sound verification on relaxed slices (2018)
  11. 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)
  12. Petiot, Guillaume; Kosmatov, Nikolai; Botella, Bernard; Giorgetti, Alain; Julliand, Jacques: How testing helps to diagnose proof failures (2018)
  13. Roux, Pierre; Iguernlala, Mohamed; Conchon, Sylvain: A non-linear arithmetic procedure for control-command software verification (2018)
  14. Summers, Alexander J.; Müller, Peter: Automating deductive verification for weak-memory programs (2018)
  15. Titolo, Laura; Feliú, Marco A.; Moscato, Mariano; Muñoz, César A.: An abstract interpretation framework for the round-off error analysis of floating-point programs (2018)
  16. Blazy, Sandrine; Bühler, David; Yakobowski, Boris: Structuring abstract interpreters through state and value abstractions (2017)
  17. Botbol, Vincent; Chailloux, Emmanuel; Le Gall, Tristan: Static analysis of communicating processes using symbolic transducers (2017)
  18. Wang, Wei; Barrett, Clark; Wies, Thomas: Partitioned memory models for program analysis (2017)
  19. Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
  20. Mandrykin, M. U.; Khoroshilov, A. V.: Region analysis for deductive verification of C programs (2016)

1 2 3 next