Why3 -- where programs meet provers
From MaRDI portal
Recommendations
Cited in
(68)- Tests and proofs for custom data generators
- A semi-automatic proof of strong connectivity
- Instrumenting a weakest precondition calculus for counterexample generation
- Why3
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Hammer for Coq: automation for dependent type theory
- The matrix reproved (verification pearl)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- Superposition with first-class booleans and inprocessing clausification
- Verifying Whiley programs with Boogie
- An automated deductive verification framework for circuit-building quantum programs
- \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages
- A verification-driven framework for iterative design of controllers
- Assumption propagation through annotated programs
- EthVer: formal verification of randomized Ethereum smart contracts
- WhyMP, a formally verified arbitrary-precision integer library
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Contract-based verification of MATLAB-style matrix programs
- Proving reachability-logic formulas incrementally
- Invariants synthesis over a combined domain for automated program verification
- Modular verification of higher-order functional programs
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Polynomial function intervals for floating-point software verification
- One logic to use them all
- Relational cost analysis in a functional-imperative setting
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
- A generic framework for symbolic execution: a coinductive approach
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- A Why3 proof of GMP algorithms
- The spirit of ghost code
- A formally proved, complete algorithm for path resolution with symbolic links
- An assertional proof of the stability and correctness of Natural Mergesort
- A generic intermediate representation for verification condition generation
- Combining top-down and bottom-up techniques in program derivation
- scientific article; zbMATH DE number 7649972 (Why is no real title available?)
- Making higher-order superposition work
- Making higher-order superposition work
- PML2: integrated program verification in ML
- 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
- \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
- Integrating ADTs in KeY and their application to history-based reasoning about collection
- scientific article; zbMATH DE number 7806141 (Why is no real title available?)
- Deductive binary code verification against source-code-level specifications
- Integrating ADTs in KeY and Their Application to History-Based Reasoning
- Formal Reasoning Using Distributed Assertions
- Verified scalable parallel computing with Why3
- Semantics, specification logic, and Hoare logic of exact real computation
- Coq support in HAHA
- Methods for deductive verification of c code using astraver toolset
- Reasoning about incompletely defined programs
- SMLtoCoq: automated generation of Coq specifications and proof obligations from SML programs with contracts
- A proof-producing compiler for blockchain applications
- An input-output relational domain for algebraic data types and functional arrays
- Automatic bit- and memory-precise verification of eBPF code
- Saturating sorting without sorts
- A formal model to prove instantiation termination for E-matching-based axiomatisations
- A methodology for modular termination verification
- Tony Hoare: his path to the ACM Turing Award
- Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
- Priority Search Trees
- Building program construction and verification tools from algebraic principles
- Formal verification of a Java component using the RESOLVE framework
- Product programs in the wild: retrofitting program verifiers to check information flow security
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)
