×

WhyML

swMATH ID: 9709
Software Authors: Filliâtre, Jean-Christophe; Paskevich, Andrei
Description: We present Why3, a tool for deductive program verification, and WhyML, its programming and specification language. WhyML is a first-order language with polymorphic types, pattern matching, and inductive predicates. Programs can make use of record types with mutable fields, type invariants, and ghost code. Verification conditions are discharged by Why3 with the help of various existing automated and interactive theorem provers. To keep verification conditions tractable and comprehensible, WhyML imposes a static control of aliases that obviates the use of a memory model. A user can write WhyML programs directly and get correct-by-construction OCaml programs via an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. We demonstrate the benefits of Why3 and WhyML on non-trivial examples of program verification.
Homepage: http://why3.lri.fr/doc-0.80/manual004.html
Related Software: Why3; z3; Coq; Isabelle/HOL; Dafny; Boogie; CVC4; VCC; GitHub; VeriFast; Spec#; Frama-C; JML; KeY; KRAKATOA; Isabelle; HOL; Eiffel; Caduceus; Viper
Cited in: 47 Documents
all top 5

Cited by 107 Authors

3 De Angelis, Emanuele
3 Fioravanti, Fabio
3 Marché, Claude
3 Pettorossi, Alberto
3 Pinto, Jorge Sousa
3 Proietti, Maurizio
2 Arusoaie, Andrei
2 Bentkamp, Alexander
2 Bian, Jinting
2 Chaudhari, Dipak L.
2 Clochard, Martin
2 Damani, Om P.
2 de Boer, Frank S.
2 De Gouw, Stijn
2 Filliâtre, Jean-Christophe
2 Frade, Maria João
2 Gondelman, Léon
2 Hiep, Hans-Dieter A.
2 Konečný, Michal
2 Lammich, Peter
2 Lourenço, Cláudio Belo
2 Paskevich, Andrei
2 Rieu-Helft, Raphaël
2 Rusu, Vlad
2 Théry, Laurent
1 Al Wardani, Farah
1 Armstrong, Alasdair
1 Bautista, Santiago
1 Baxter, James
1 Bertot, Yves
1 Blanchette, Jasmin Christian
1 Boström, Pontus
1 Brauße, Franz
1 Chaudhuri, Kaustuv
1 Chechik, Marsha
1 Chen, Ran
1 Chin, Wei-Ngan
1 Collins, Peter J.
1 Cruanes, Simon
1 Czajka, Łukasz
1 Dailler, Sylvain
1 Dubois, Catherine
1 Duracz, Jan
1 Eilers, Marco
1 Foster, Simon
1 Fuchs, Laurent
1 Gaboardi, Marco
1 Gallagher, John P.
1 Garg, Deepak
1 Ghezzi, Carlo
1 Giorgetti, Alain
1 Gomes, Victor B. F.
1 Groves, Lindsay J.
1 Hauzar, David
1 He, Guanhua
1 Hermenegildo, Manuel V.
1 Jeannerod, Nicolas
1 Kaliszyk, Cezary
1 Kamkin, Alexander
1 Khoroshilov, Alexey
1 Kim, Sunyoung
1 Kobayashi, Naoki
1 Kosmatov, Nikolai
1 Kotsynyak, Artem
1 Le Gall, Pascale
1 Léchenet, Jean-Christophe
1 Lee, Gyesik
1 Leino, K. Rustan M.
1 Lucanu, Dorel
1 Lucio, Paqui
1 Mazurek, Łukasz
1 Meier, Severin
1 Melquiond, Guillaume
1 Menghi, Claudio
1 Miller, Dale Allen
1 Montagu, Benoît
1 Montenegro, Manuel
1 Moy, Yannick
1 Müller, Norbert Th.
1 Müller, Peter
1 Neumann, Eike
1 Nipkow, Tobias
1 Nummelin, Visa
1 Park, Sewon
1 Pearce, David J.
1 Peña, Ricardo
1 Preining, Norbert
1 Putro, Pavel
1 Qin, Shengchao
1 Qu, Weihao
1 Rideau, Laurence
1 Rumreich, Laine
1 Sánchez-Hernández, Jaime
1 Sato, Ryosuke
1 Sefidgar, S. Reza
1 Sheng, Huanhuan
1 Sivilotti, Paolo A. G.
1 Spoletini, Paola
1 Struth, Georg
1 Tourret, Sophie
...and 7 more Authors
all top 5

Cited in 13 Serials

6 Journal of Automated Reasoning
5 Formal Aspects of Computing
2 Journal of Symbolic Computation
2 Formal Methods in System Design
2 Theory and Practice of Logic Programming
2 Journal of Formalized Reasoning
2 Journal of Logical and Algebraic Methods in Programming
1 Theoretical Computer Science
1 Advances in Applied Clifford Algebras
1 Journal of Functional Programming
1 Annals of Mathematics and Artificial Intelligence
1 ACM Transactions on Computational Logic
1 Logical Methods in Computer Science
all top 5

Cited in 9 Fields

46 Computer science (68-XX)
9 Mathematical logic and foundations (03-XX)
4 Numerical analysis (65-XX)
2 Number theory (11-XX)
2 Operations research, mathematical programming (90-XX)
1 Combinatorics (05-XX)
1 Linear and multilinear algebra; matrix theory (15-XX)
1 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
1 Information and communication theory, circuits (94-XX)

Citations by Year