Why3 -- where programs meet provers
From MaRDI portal
Publication:5326280
DOI10.1007/978-3-642-37036-6_8zbMATH Open1435.68366OpenAlexW1820726602MaRDI QIDQ5326280FDOQ5326280
Authors: Jean-Christophe Filliâtre, Andrei Paskevich 
Publication date: 5 August 2013
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-37036-6_8
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cited In (55)
- Verifying Whiley programs with Boogie
- Formal verification of a Java component using the RESOLVE framework
- Product programs in the wild: retrofitting program verifiers to check information flow security
- EthVer: formal verification of randomized Ethereum smart contracts
- PML2: integrated program verification in ML
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- A formally proved, complete algorithm for path resolution with symbolic links
- WhyMP, a formally verified arbitrary-precision integer library
- Contract-based verification of MATLAB-style matrix programs
- Tests and proofs for custom data generators
- Lifting numeric relational domains to algebraic data types
- An automated deductive verification framework for circuit-building quantum programs
- \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages
- A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- A semi-automatic proof of strong connectivity
- Assumption propagation through annotated programs
- Efficient computation of arbitrary control dependencies
- Why3-do: the way of harmonious distributed system proofs
- Making higher-order superposition work
- Building program construction and verification tools from algebraic principles
- Combining top-down and bottom-up techniques in program derivation
- Title not available (Why is that?)
- \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Instrumenting a weakest precondition calculus for counterexample generation
- Integrating ADTs in KeY and their application to history-based reasoning about collection
- A Why3 proof of GMP algorithms
- Polynomial function intervals for floating-point software verification
- Integrating ADTs in KeY and Their Application to History-Based Reasoning
- Why3
- Making higher-order superposition work
- Superposition with first-class booleans and inprocessing clausification
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
- Proving reachability-logic formulas incrementally
- A generic intermediate representation for verification condition generation
- Modular verification of higher-order functional programs
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- A generic framework for symbolic execution: a coinductive approach
- One logic to use them all
- A verification-driven framework for iterative design of controllers
- Deductive binary code verification against source-code-level specifications
- The matrix reproved (verification pearl)
- Hammer for Coq: automation for dependent type theory
- Invariants synthesis over a combined domain for automated program verification
- Relational cost analysis in a functional-imperative setting
- Title not available (Why is that?)
- The spirit of ghost code
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- An assertional proof of the stability and correctness of Natural Mergesort
- Semantics, specification logic, and Hoare logic of exact real computation
- Formal Reasoning Using Distributed Assertions
- Verified scalable parallel computing with Why3
Uses Software
This page was built for publication: Why3 -- where programs meet provers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5326280)
