···

       
8
       
8
       
 
       
- an analyzer based on abstract interpretation (Eva plug-in);

     

       
9
       
9
       
 
       
- a program proof framework based on weakest precondition calculus (WP plug-in);

     

       
10
       
10
       
 
       
- a program slicer (Slicing plug-in);

     

       
11
       
11
       
-
       
- a tool for verification of temporal (LTL) properties (Aoraï plug-in);

     

       
11
       
11
       
+
       
- a tool for verification of automata-based properties (Aoraï plug-in);

     

       
12
       
12
       
 
       
- a runtime verification tool (E-ACSL plug-in);

     

       
13
       
13
       
 
       
- several tools for code base exploration and dependency analysis

     

       
14
       
14
       
 
       
  (plug-ins From, Impact, Metrics, Occurrence, Scope, etc.).

     
···

       
43
       
43
       
 
       
  "Alexander Kogtenkov"

     

       
44
       
44
       
 
       
  "Remi Lazarini"

     

       
45
       
45
       
 
       
  "Tristan Le Gall"

     

       
46
       
46
       
+
       
  "Kilyan Le Gallic"

     

       
46
       
47
       
 
       
  "Jean-Christophe Léchenet"

     

       
47
       
48
       
 
       
  "Matthieu Lemerre"

     

       
48
       
49
       
 
       
  "Dara Ly"

     
···

       
65
       
66
       
 
       
  "Virgile Robles"

     

       
66
       
67
       
 
       
  "Jan Rochel"

     

       
67
       
68
       
 
       
  "Muriel Roger"

     

       
69
       
69
       
+
       
  "Cécile Ruet-Cros"

     

       
68
       
70
       
 
       
  "Julien Signoles"

     

       
69
       
71
       
 
       
  "Nicolas Stouls"

     

       
70
       
72
       
 
       
  "Kostyantyn Vorobyov"

     
···

       
73
       
75
       
 
       
homepage: "https://frama-c.com/"

     

       
74
       
76
       
 
       
license: "LGPL-2.1-only"

     

       
75
       
77
       
 
       
dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"

     

       
76
       
76
       
-
       
doc: "http://frama-c.com/download/user-manual-29.0-Copper.pdf"

     

       
78
       
78
       
+
       
doc: "https://frama-c.com/download/user-manual-30.0-Zinc.pdf"

     

       
77
       
79
       
 
       
bug-reports: "https://git.frama-c.com/pub/frama-c/issues"

     

       
78
       
80
       
 
       
tags: [

     

       
79
       
79
       
-
       
  "deductive"

     

       
81
       
81
       
+
       
  "deductive verification"

     

       
80
       
82
       
 
       
  "program verification"

     

       
81
       
83
       
 
       
  "formal specification"

     

       
82
       
84
       
 
       
  "automated theorem prover"

     
···

       
173
       
175
       
 
       
Recommended provers are:

     

       
174
       
176
       
 
       
- Alt-Ergo (https://alt-ergo.ocamlpro.com)

     

       
175
       
177
       
 
       
- CVC4     (https://cvc4.github.io)

     

       
178
       
178
       
+
       
- CVC5     (https://cvc5.github.io)

     

       
176
       
179
       
 
       
- Z3       (https://github.com/Z3Prover/z3)

     

       
177
       
180
       
 
       
Use 'why3 config detect' to configure new provers.

     

       
178
       
181
       
 
       
 " { success }

     
···

       
186
       
189
       
 
       
]

     

       
187
       
190
       
 
       


     

       
188
       
191
       
 
       
url {

     

       
189
       
189
       
-
       
  src: "https://www.frama-c.com/download/frama-c-30.0-TEST-Zinc.tar.gz"

     

       
190
       
190
       
-
       
  checksum: "sha256=fdef89786e833ae9d1392f21f624bd949ae34f83d6d1284f6a4d8921758578b4"

     

       
192
       
192
       
+
       
  src: "https://www.frama-c.com/download/frama-c-30.0-Zinc.tar.gz"

     

       
193
       
193
       
+
       
  checksum: "sha256=3ac0f995261ec829a7bd042bf70fc29ac6379029eb9df30bcc044748eb4d2a56"

     

       
191
       
194
       
 
       
}