×

Why3

swMATH ID: 4438
Software Authors: François Bobot; Jean-Christophe Filliâtre; Claude Marché; Guillaume Melquiond; Andrei Paskevich
Description: Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.
Homepage: http://why3.lri.fr/
Keywords: program verification
Related Software: KRAKATOA; Coq; Caduceus; z3; Boogie; Isabelle/HOL; WhyML; Spec#; Dafny; VCC; Frama-C; JML; VeriFast; Isabelle; SIMPLIFY; cvc3; ESC/Java; Alt-Ergo; CVC4; ACSL
Cited in: 128 Publications
Further Publications: http://why3.lri.fr/#publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Why3 – where programs meet provers. Zbl 1435.68366
Filliâtre, Jean-Christophe; Paskevich, Andrei
2013
all top 5

Cited by 243 Authors

10 Marché, Claude
9 Filliâtre, Jean-Christophe
7 Melquiond, Guillaume
6 Leino, K. Rustan M.
5 Böhme, Sascha
5 Rieu-Helft, Raphaël
4 Blanchette, Jasmin Christian
4 Boldo, Sylvie
4 Kaliszyk, Cezary
4 Moy, Yannick
4 Paskevich, Andrei
3 Pinto, Jorge Sousa
3 Smallbone, Nicholas
3 Swamy, Nikhil
3 Wies, Thomas
3 Wolff, Burkhart
2 Ahrendt, Wolfgang
2 Arusoaie, Andrei
2 Barbosa, Manuel
2 Benzaken, Véronique
2 Bhargavan, Karthikeyan
2 Chaudhari, Dipak L.
2 Chechik, Marsha
2 Chen, Ran
2 Clément, François
2 Clochard, Martin
2 Conchon, Sylvain
2 Contejean, Evelyne
2 Cristiá, Maximiliano
2 Damani, Om P.
2 Fournet, Cédric
2 Frade, Maria João
2 Giorgino, Mathieu
2 Gondelman, Léon
2 Halmagrand, Pierre
2 Hriţcu, Cătălin
2 Khan, Muhammad Taimoor
2 Kobayashi, Naoki
2 Mayero, Micaela
2 Müller, Peter
2 Peña, Ricardo
2 Popescu, Andrei
2 Rastogi, Aseem
2 Reynolds, Andrew
2 Rossi, Gianfranco
2 Roşu, Grigore
2 Rusu, Vlad
2 Schreiner, Wolfgang
2 Schulte, Wolfram
2 Siegel, Stephen F.
2 Strecker, Martin
2 Strub, Pierre-Yves
2 Summers, Alexander J.
2 Théry, Laurent
2 Ulbrich, Mattias
2 Urban, Josef
2 Weis, Pierre
2 Zirkel, Timothy K.
1 Abbasi, Rosa
1 Abed, Sa’ed
1 Affeldt, Reynald
1 Ahman, Danel
1 Aït Mohamed, Otmane
1 Alkassar, Eyad
1 Anureev, Igor’ Sergeevich
1 Armstrong, Alasdair
1 Aspinall, David
1 Ayad, Ali
1 Bacelar Almeida, José
1 Bansal, Kshitij
1 Baro, Sylvain
1 Barrett, Clark W.
1 Baxter, James
1 Berghammer, Rudolf
1 Beringer, Lennart
1 Bertot, Yves
1 Blazy, Sandrine
1 Blot, Arthur
1 Bobot, François
1 Boström, Pontus
1 Boulmé, Sylvain
1 Brady, Edwin C.
1 Brumley, Billy Bob
1 Bubel, Richard
1 Bulwahn, Lukas
1 Burel, Guillaume
1 Bury, Guillaume
1 Cauderlier, Raphaël
1 Chalin, Patrice
1 Chen, Juan
1 Chin, Wei-Ngan
1 Ciobâcă, Ştefan
1 Collavizza, Hélène
1 Cruanes, Simon
1 Czajka, Łukasz
1 Dagand, Pierre-Evariste
1 Dailler, Sylvain
1 Darulova, Eva
1 Daum, Matthias
1 De Angelis, Emanuele
...and 143 more Authors

Citations by Year