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 50 articles )
Showing results 1 to 20 of 50.
Sorted by year (- Armstrong, Alasdair; Gomes, Victor B.F.; Struth, Georg: Building program construction and verification tools from algebraic principles (2016)
- Halmagrand, Pierre: Soundly proving B method formulæusing typed sequent calculus (2016)
- Totla, Nishant; Wies, Thomas: Complete instantiation-based interpolation (2016)
- Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
- Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Tool-based verification of a relational vertex coloring program (2015)
- Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015)
- Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
- Benzaken, Véronique; Contejean, Évelyne; Dumbrava, Stefania: A Coq formalization of the relational data model (2014)
- Betelin, V.; Galatenko, V.; Kostyukhin, K.: Controlled execution with explicit model (2014)
- Dockins, Robert; Tolmach, Andrew: suppl: a flexible language for policies (2014)
- Dufourd, Jean-François: Hypermap specification and certified linked implementation using orbits (2014)
- Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
- Fuchs, Laurent; Théry, Laurent: Implementing geometric algebra products with binary trees (2014)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
- Almeida, J.Bacelar; Barbosa, Manuel; Pinto, Jorge S.; Vieira, Bárbara: Formal verification of side-channel countermeasures using self-composition (2013)
- Blanchette, Jasmin Christian; Paskevich, Andrei: TFF1: the TPTP typed first-order form with rank-1 polymorphism (2013)
- Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Wave equation numerical resolution: a comprehensive mechanized proof of a C program (2013)
- Felleisen, Matthias (ed.); Gardner, Philippa (ed.): Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16--24, 2013. Proceedings (2013)
- Filli^atre, Jean-Christophe; Paskevich, Andrei: Why3 -- where programs meet provers (2013)
- Leino, K.Rustan M.: Automating theorem proving with SMT (2013)
Further publications can be found at: http://why3.lri.fr/#publications