Why3 -- where programs meet provers
From MaRDI portal
Publication:5326280
Recommendations
Cited in
(55)- An assertional proof of the stability and correctness of Natural Mergesort
- 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
- Semantics, specification logic, and Hoare logic of exact real computation
- 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
- Contract-based verification of MATLAB-style matrix programs
- Tests and proofs for custom data generators
- WhyMP, a formally verified arbitrary-precision integer library
- An automated deductive verification framework for circuit-building quantum programs
- \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages
- Lifting numeric relational domains to algebraic data types
- A semi-automatic proof of strong connectivity
- A verified VCGen based on dynamic logic: an exercise in meta-verification with Why3
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Assumption propagation through annotated programs
- Efficient computation of arbitrary control dependencies
- Why3-do: the way of harmonious distributed system proofs
- Building program construction and verification tools from algebraic principles
- Making higher-order superposition work
- Combining top-down and bottom-up techniques in program derivation
- scientific article; zbMATH DE number 7806141 (Why is no real title available?)
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
- Instrumenting a weakest precondition calculus for counterexample generation
- Polynomial function intervals for floating-point software verification
- Integrating ADTs in KeY and their application to history-based reasoning about collection
- Why3
- A Why3 proof of GMP algorithms
- Integrating ADTs in KeY and Their Application to History-Based Reasoning
- Superposition with first-class booleans and inprocessing clausification
- Making higher-order superposition work
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- Proving reachability-logic formulas incrementally
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
- 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
- Formal Reasoning Using Distributed Assertions
- One logic to use them all
- A verification-driven framework for iterative design of controllers
- The matrix reproved (verification pearl)
- Deductive binary code verification against source-code-level specifications
- Hammer for Coq: automation for dependent type theory
- Invariants synthesis over a combined domain for automated program verification
- The spirit of ghost code
- Relational cost analysis in a functional-imperative setting
- scientific article; zbMATH DE number 7649972 (Why is no real title available?)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Verified scalable parallel computing with Why3
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)
