Why3
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.
Keywords for this software
References in zbMATH (referenced in 131 articles , 1 standard article )
Showing results 1 to 20 of 131.
Sorted by year (- Filliâtre, Jean-Christophe: Simpler proofs with decentralized invariants (2021)
- Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier: First-order automated reasoning with theories: when deduction modulo theory meets practice (2020)
- Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
- Ishii, Daisuke; Yabu, Tomohito: Computer-assisted verification of four interval arithmetic operators (2020)
- Melquiond, Guillaume; Rieu-Helft, Raphaël: WhyMP, a formally verified arbitrary-precision integer library (2020)
- Peña, Ricardo: An assertional proof of red-black trees using Dafny (2020)
- Lammich, Peter; Sefidgar, S. Reza: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (2019)
- Menghi, Claudio; Spoletini, Paola; Chechik, Marsha; Ghezzi, Carlo: A verification-driven framework for iterative design of controllers (2019)
- Rieu-Helft, Raphaël: A Why3 proof of GMP algorithms (2019)
- Schulz, Stephan; Cruanes, Simon; Vukmirović, Petar: Faster, higher, stronger: E 2.3 (2019)
- Wang, Wenxi; Søndergaard, Harald; Stuckey, Peter J.: Wombit: a portfolio bit-vector solver using word-level propagation (2019)
- Benzaken, V.; Contejean, É.; Keller, Ch.; Martins, E.: A Coq formalisation of SQL’s execution engines (2018)
- Bertot, Yves; Rideau, Laurence; Théry, Laurent: Distant decimals of (\pi): formal proofs of some algorithms computing them and guarantees of exact computation (2018)
- Blazy, Sandrine (ed.); Chechik, Marsha (ed.): Selected extended papers of VSTTE 2016 (2018)
- Clochard, Martin; Gondelman, Léon; Pereira, Mário: The matrix reproved (verification pearl) (2018)
- Cristiá, Maximiliano; Rossi, Gianfranco: A set solver for finite set relation algebra (2018)
- Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
- Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
- Dubois, Catherine; Giorgetti, Alain: Tests and proofs for custom data generators (2018)
- Grigoriy Volkov, Mikhail Mandrykin, Denis Efremov: Lemma Functions for Frama-C: C Programs as Proofs (2018) arXiv
Further publications can be found at: http://why3.lri.fr/#publications