Cited in
(91)- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
- Proving reachability-logic formulas incrementally
- A formally proved, complete algorithm for path resolution with symbolic links
- A generic intermediate representation for verification condition generation
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Assumption propagation through annotated programs
- Making higher-order superposition work
- A Why3 proof of GMP algorithms
- Invariants synthesis over a combined domain for automated program verification
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- SableJBDD
- checkbashisms
- A verification-driven framework for iterative design of controllers
- BDD
- JDD
- A formally verified interpreter for a shell-like programming language
- Formal verification of a Java component using the RESOLVE framework
- Product programs in the wild: retrofitting program verifiers to check information flow security
- A generic framework for symbolic execution: a coinductive approach
- Contract-based verification of MATLAB-style matrix programs
- WhyMP, a formally verified arbitrary-precision integer library
- EthVer: formal verification of randomized Ethereum smart contracts
- Building program construction and verification tools from algebraic principles
- Relational cost analysis in a functional-imperative setting
- Combining top-down and bottom-up techniques in program derivation
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Implementing geometric algebra products with binary trees
- Tests and proofs for custom data generators
- Apron
- Cocktail
- Dafny
- RealLib
- Frama-C
- Why3
- Alt-Ergo
- core 2
- Netsoft
- FocalTest
- VCC
- Boogie
- Chalice
- PolyPaver
- KeY
- FixBag
- BWare
- Ciao
- CiaoPP
- Clados
- BVD
- VCGen
- THOR
- CacBDD
- OpenJML
- Luck
- VeriFun
- VeriMAP
- LiquidHaskell
- Bedrock
- TiML
- Dijkstra Shortest Path
- Flow Networks
- Guardol
- Equations
- Focalide
- AutoProof
- RVT
- Logipedia
- Simpl
- Instrumenting a weakest precondition calculus for counterexample generation
- An assertional proof of the stability and correctness of Natural Mergesort
- Manticore
- HACL*
- WhyMP
- FreeSpec
- Binutils
- Mythril
- Prpu_Maxflow
- Daisy
- Why3 -- where programs meet provers
- scientific article; zbMATH DE number 7649972 (Why is no real title available?)
- Verifying Whiley programs with Boogie
- The spirit of ghost code
- CoLiS
- Shellcheck
- EthVer
- solgraph
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Hammer for Coq: automation for dependent type theory
- Modular verification of higher-order functional programs
- The matrix reproved (verification pearl)
- Polynomial function intervals for floating-point software verification
This page was built for software: WhyML
