package frama-c

  1. Overview
  2. No Docs
Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Edit opam file Versions (34)

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. L
    Lionel Blatter
  6. F
    François Bobot
  7. R
    Richard Bonichon
  8. Q
    Quentin Bouillaguet
  9. D
    David Bühler
  10. Z
    Zakaria Chihani
  11. L
    Loïc Correnson
  12. J
    Julien Crétin
  13. P
    Pascal Cuoq
  14. Z
    Zaynah Dargaye
  15. J
    Jean-Christophe Filliâtre
  16. P
    Philippe Herrmann
  17. M
    Maxime Jacquemin
  18. F
    Florent Kirchner
  19. T
    Tristan Le Gall
  20. J
    Jean-Christophe Léchenet
  21. M
    Matthieu Lemerre
  22. D
    David Maison
  23. C
    Claude Marché
  24. A
    André Maroneze
  25. M
    Melody Méaulle
  26. B
    Benjamin Monate
  27. Y
    Yannick Moy
  28. A
    Anne Pacalet
  29. V
    Valentin Perrelle
  30. G
    Guillaume Petiot
  31. V
    Virgile Prevosto
  32. A
    Armand Puccetti
  33. M
    Muriel Roger
  34. J
    Julien Signoles
  35. K
    Kostyantyn Vorobyov
  36. B
    Boris Yakobowski

Maintainers

  1. F
    francois.bobot@cea.fr

Sources

frama-c-18.0-Argon.tar.gz
md5=659cf094d6e92a8adeb5863ec229020b

Description

Frama-C gathers several analysis techniques in a single collaborative framework, based on analyzers (called "plug-ins") that can build upon the results computed by other analyzers in the framework. Thanks to this approach, Frama-C provides sophisticated tools, including:

  • an analyzer based on abstract interpretation (Eva plug-in);
  • a program proof framework based on weakest precondition calculus (WP plug-in);
  • a program slicer (Slicing plug-in);
  • a tool for verification of temporal (LTL) properties (Aoraï plug-in);
  • a runtime verification tool (E-ACSL plug-in);
  • several tools for code base exploration and dependency analysis (plug-ins From, Impact, Metrics, Occurrence, Scope, etc.). These plug-ins communicate between each other via the Frama-C API and via ACSL (ANSI/ISO C Specification Language) properties.

Tags

deductive program verification formal specification automated theorem prover interactive theorem prover C plugins abstract interpretation slicing weakest precondition ACSL dataflow analysis runtime verification

Published: 30 Nov 2018

Dev Dependencies

None

Used by (2)

  1. pilat < "1.3"
  2. why < "2.32"

Conflicts (6)

  1. frama-c-base
  2. frama-c-e-acsl
  3. lablgtk < "2.18.2"
  4. coq < "8.4.6"
  5. why3 >= "1.0.0"
  6. why3-base < "0.88"