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 89 articles , 1 standard article )
Showing results 1 to 20 of 89.
Sorted by year (- Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
- Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
- Müller, Dennis; Gauthier, Thibault; Kaliszyk, Cezary; Kohlhase, Michael; Rabe, Florian: Classification of alignments between concepts of formal mathematical systems (2017)
- Sato, Ryosuke; Kobayashi, Naoki: Modular verification of higher-order functional programs (2017)
- Armstrong, Alasdair; Gomes, Victor B.F.; Struth, Georg: Building program construction and verification tools from algebraic principles (2016)
- Belo Lourenço, Cláudio; João Frade, Maria; Sousa Pinto, Jorge: Formalizing single-assignment program verification: an adaptation-complete approach (2016)
- Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
- Blot, Arthur; Dagand, Pierre-Évariste; Lawall, Julia: From sets to bits in Coq (2016)
- Filli^atre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei: The spirit of ghost code (2016)
- Halmagrand, Pierre: Soundly proving B method formulæusing typed sequent calculus (2016)
- Müller, Peter; Schwerhoff, Malte; Summers, Alexander J.: Viper: a verification infrastructure for permission-based reasoning (2016)
- Rusu, Vlad; Arusoaie, Andrei: Proving reachability-logic formulas incrementally (2016)
- Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim; Zanella-Béguelin, Santiago: Dependent types and multi-monadic effects in $\mathrmF^*$ (2016)
- Totla, Nishant; Wies, Thomas: Complete instantiation-based interpolation (2016)
- Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
- Bansal, Kshitij; Reynolds, Andrew; King, Tim; Barrett, Clark; Wies, Thomas: Deciding local theory extensions via E-matching (2015)
- Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Tool-based verification of a relational vertex coloring program (2015)
- Chaudhari, Dipak L.; Damani, Om: Combining top-down and bottom-up techniques in program derivation (2015)
- Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
- Leino, K.Rustan M.; Lucio, Paqui: An assertional proof of the stability and correctness of Natural Mergesort (2015)
Further publications can be found at: http://why3.lri.fr/#publications