Why3 — Where Programs Meet Provers
From MaRDI portal
Publication:5326280
DOI10.1007/978-3-642-37036-6_8zbMath1435.68366OpenAlexW1820726602MaRDI QIDQ5326280
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
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (45)
An Assertional Proof of the Stability and Correctness of Natural Mergesort ⋮ Verifying Catamorphism-Based Contracts using Constrained Horn Clauses ⋮ Contract-based verification of MATLAB-style matrix programs ⋮ Tests and proofs for custom data generators ⋮ Formal verification of a Java component using the RESOLVE framework ⋮ Product programs in the wild: retrofitting program verifiers to check information flow security ⋮ Unnamed Item ⋮ Assumption propagation through annotated programs ⋮ Instrumenting a weakest precondition calculus for counterexample generation ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ Hammer for Coq: automation for dependent type theory ⋮ EthVer: formal verification of randomized Ethereum smart contracts ⋮ WhyMP, a formally verified arbitrary-precision integer library ⋮ Automated Algebraic Reasoning for Collections and Local Variables with Lenses ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3 ⋮ Lifting numeric relational domains to algebraic data types ⋮ Efficient computation of arbitrary control dependencies ⋮ Why3-do: the way of harmonious distributed system proofs ⋮ Unnamed Item ⋮ \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic ⋮ Integrating ADTs in KeY and their application to history-based reasoning about collection ⋮ The matrix reproved (verification pearl) ⋮ Polynomial function intervals for floating-point software verification ⋮ Unnamed Item ⋮ Formalizing network flow algorithms: a refinement approach in Isabelle/HOL ⋮ Modular Verification of Higher-Order Functional Programs ⋮ An automated deductive verification framework for circuit-building quantum programs ⋮ \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ The spirit of ghost code ⋮ A Generic Intermediate Representation for Verification Condition Generation ⋮ Combining Top-Down and Bottom-Up Techniques in Program Derivation ⋮ Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach ⋮ Building program construction and verification tools from algebraic principles ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Why3 ⋮ Proving Reachability-Logic Formulas Incrementally ⋮ Unnamed Item ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification ⋮ A verification-driven framework for iterative design of controllers ⋮ Verifying Whiley programs with Boogie ⋮ Relational cost analysis in a functional-imperative setting
Uses Software
This page was built for publication: Why3 — Where Programs Meet Provers
