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.


References in zbMATH (referenced in 55 articles )

Showing results 1 to 20 of 55.
Sorted by year (citations)

1 2 3 next

  1. Chaudhari, Dipak L.; Damani, Om: Assumption propagation through annotated programs (2017)
  2. Armstrong, Alasdair; Gomes, Victor B.F.; Struth, Georg: Building program construction and verification tools from algebraic principles (2016)
  3. Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas: Encoding monomorphic and polymorphic types (2016)
  4. Filli^atre, Jean-Christophe; Gondelman, Léon; Paskevich, Andrei: The spirit of ghost code (2016)
  5. Halmagrand, Pierre: Soundly proving B method formulæusing typed sequent calculus (2016)
  6. Totla, Nishant; Wies, Thomas: Complete instantiation-based interpolation (2016)
  7. Wiik, Jonatan; Boström, Pontus: Contract-based verification of MATLAB-style matrix programs (2016)
  8. Berghammer, Rudolf; Höfner, Peter; Stucke, Insa: Tool-based verification of a relational vertex coloring program (2015)
  9. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  10. Rosén, Dan; Smallbone, Nicholas: TIP: tools for inductive provers (2015)
  11. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  12. Benzaken, Véronique; Contejean, Évelyne; Dumbrava, Stefania: A Coq formalization of the relational data model (2014)
  13. Betelin, V.; Galatenko, V.; Kostyukhin, K.: Controlled execution with explicit model (2014) ioport
  14. David R. Cok: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse (2014) arXiv
  15. Dockins, Robert; Tolmach, Andrew: suppl: a flexible language for policies (2014)
  16. Dufourd, Jean-François: Hypermap specification and certified linked implementation using orbits (2014)
  17. Duracz, Jan; Konečný, Michal: Polynomial function intervals for floating-point software verification (2014)
  18. Fuchs, Laurent; Théry, Laurent: Implementing geometric algebra products with binary trees (2014)
  19. Kaliszyk, Cezary; Urban, Josef: Learning-assisted automated reasoning with $\mathsfFlyspeck$ (2014)
  20. Almeida, J.Bacelar; Barbosa, Manuel; Pinto, Jorge S.; Vieira, Bárbara: Formal verification of side-channel countermeasures using self-composition (2013)

1 2 3 next


Further publications can be found at: http://why3.lri.fr/#publications