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 105 articles , 1 standard article )
Showing results 1 to 20 of 105.
Sorted by year (- Bertot, Yves; Rideau, Laurence; Théry, Laurent: Distant decimals of $\pi $: formal proofs of some algorithms computing them and guarantees of exact computation (2018)
- Clochard, Martin; Gondelman, Léon; Pereira, Mário: The matrix reproved (verification pearl) (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
- Kojima, Kensuke; Imanishi, Akifumi; Igarashi, Atsushi: Automated verification of functional correctness of race-free GPU programs (2018)
- Kotelnikov, Evgenii; Kovács, Laura; Voronkov, Andrei: A foolish encoding of the next state relations of imperative programs (2018)
- Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil: Dijkstra monads for free (2017)
- Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
- Chen, Ran; Lévy, Jean-Jacques: A semi-automatic proof of strong connectivity (2017)
- Fumex, Clément; Marché, Claude; Moy, Yannick: Automating the verification of floating-point programs (2017)
- Jeannerod, Nicolas; Marché, Claude; Treinen, Ralf: A formally verified interpreter for a shell-like programming language (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)
- Rieu-Helft, Raphaël; Marché, Claude; Melquiond, Guillaume: How to get an efficient yet verified arbitrary-precision integer library (2017)
- Sato, Ryosuke; Kobayashi, Naoki: Modular verification of higher-order functional programs (2017)
- Schoolderman, Marc: Verifying branch-free assembly code in Why3 (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)
Further publications can be found at: http://why3.lri.fr/#publications