Cited in
(91)- 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
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- 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
- Assumption propagation through annotated programs
- Building program construction and verification tools from algebraic principles
- Combining top-down and bottom-up techniques in program derivation
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Instrumenting a weakest precondition calculus for counterexample generation
- Polynomial function intervals for floating-point software verification
- 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
- Implementing geometric algebra products with binary trees
- CacBDD
- OpenJML
- Luck
- VeriFun
- VeriMAP
- LiquidHaskell
- Bedrock
- TiML
- Dijkstra Shortest Path
- Flow Networks
- Guardol
- Equations
- Focalide
- AutoProof
- RVT
- Logipedia
- Simpl
- Manticore
- HACL*
- WhyMP
- FreeSpec
- Binutils
- Mythril
- Prpu_Maxflow
- Daisy
- A Why3 proof of GMP algorithms
- Making higher-order superposition work
- BDD
- JDD
- Proving reachability-logic formulas incrementally
- SableJBDD
- 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
- CoLiS
- Shellcheck
- EthVer
- solgraph
- A formally verified interpreter for a shell-like programming language
- A verification-driven framework for iterative design of controllers
- checkbashisms
- The matrix reproved (verification pearl)
- Hammer for Coq: automation for dependent type theory
- Invariants synthesis over a combined domain for automated program verification
- Why3 -- where programs meet provers
- 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
This page was built for software: WhyML
