WhyML
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.
Keywords for this software
References in zbMATH (referenced in 25 articles )
Showing results 1 to 20 of 25.
Sorted by year (- 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)
- 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)
- Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
- Chen, Ran; Clochard, Martin; Marché, Claude: A formally proved, complete algorithm for path resolution with symbolic links (2017)
- Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (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)
- Filliâtre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei: The spirit of ghost code (2016)
- Rusu, Vlad; Arusoaie, Andrei: Proving reachability-logic formulas incrementally (2016)
- Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
- 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)