×

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: Coq; KRAKATOA; z3; Caduceus; WhyML; Boogie; Isabelle/HOL; Dafny; Spec#; JML; Frama-C; VCC; VeriFast; Isabelle; CVC4; SIMPLIFY; cvc3; ESC/Java; TPTP; Alt-Ergo
Cited in: 144 Documents
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 267 Authors

10 Marché, Claude
9 Filliâtre, Jean-Christophe
7 Melquiond, Guillaume
6 Blanchette, Jasmin Christian
6 Leino, K. Rustan M.
5 Böhme, Sascha
5 Pinto, Jorge Sousa
5 Rieu-Helft, Raphaël
4 Bentkamp, Alexander
4 Boldo, Sylvie
4 Kaliszyk, Cezary
4 Moy, Yannick
4 Paskevich, Andrei
4 Vukmirović, Petar
3 Chen, Ran
3 Cruanes, Simon
3 De Angelis, Emanuele
3 Fioravanti, Fabio
3 Frade, Maria João
3 Müller, Peter
3 Nummelin, Visa
3 Pettorossi, Alberto
3 Proietti, Maurizio
3 Smallbone, Nicholas
3 Swamy, Nikhil
3 Théry, Laurent
3 Tourret, Sophie
3 Wies, Thomas
3 Wolff, Burkhart
2 Ahrendt, Wolfgang
2 Arusoaie, Andrei
2 Barbosa, Manuel
2 Benzaken, Véronique
2 Bhargavan, Karthikeyan
2 Bian, Jinting
2 Chaudhari, Dipak L.
2 Chechik, Marsha
2 Clément, François
2 Clochard, Martin
2 Conchon, Sylvain
2 Contejean, Evelyne
2 Cristiá, Maximiliano
2 Damani, Om P.
2 de Boer, Frank S.
2 De Gouw, Stijn
2 Fournet, Cédric
2 Giorgino, Mathieu
2 Gondelman, Léon
2 Halmagrand, Pierre
2 Hiep, Hans-Dieter A.
2 Hriţcu, Cătălin
2 Khan, Muhammad Taimoor
2 Kobayashi, Naoki
2 Lammich, Peter
2 Levy, Jean-Jacques
2 Lourenço, Cláudio Belo
2 Mayero, Micaela
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 Ulbrich, Mattias
2 Urban, Josef
2 Weis, Pierre
2 Zhan, Bohua
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 Bautista, Santiago
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.
...and 167 more Authors

Citations by Year