The following pages link to WhyML (Q21688):
Displaying 35 items.
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- Polynomial function intervals for floating-point software verification (Q457251) (← links)
- A generic framework for symbolic execution: a coinductive approach (Q507361) (← links)
- The spirit of ghost code (Q518394) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- Formal verification of a Java component using the RESOLVE framework (Q831953) (← links)
- Product programs in the wild: retrofitting program verifiers to check information flow security (Q832225) (← links)
- Tests and proofs for custom data generators (Q1624592) (← links)
- A formally verified interpreter for a shell-like programming language (Q1630019) (← links)
- Instrumenting a weakest precondition calculus for counterexample generation (Q1648649) (← links)
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- The matrix reproved (verification pearl) (Q1703015) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- A verification-driven framework for iterative design of controllers (Q2335947) (← links)
- Assumption propagation through annotated programs (Q2628303) (← links)
- EthVer: formal verification of randomized Ethereum smart contracts (Q2670859) (← links)
- WhyMP, a formally verified arbitrary-precision integer library (Q2673999) (← links)
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach (Q2802468) (← links)
- Proving Reachability-Logic Formulas Incrementally (Q2827839) (← links)
- Invariants Synthesis over a Combined Domain for Automated Program Verification (Q2842643) (← links)
- Modular Verification of Higher-Order Functional Programs (Q2988670) (← links)
- Relational cost analysis in a functional-imperative setting (Q5020903) (← links)
- Verifying Catamorphism-Based Contracts using Constrained Horn Clauses (Q5038461) (← links)
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses (Q5098716) (← links)
- (Q5130751) (← links)
- (Q5195286) (← links)
- An Assertional Proof of the Stability and Correctness of Natural Mergesort (Q5277907) (← links)
- Why3 — Where Programs Meet Provers (Q5326280) (← links)
- A Generic Intermediate Representation for Verification Condition Generation (Q5743596) (← links)
- Combining Top-Down and Bottom-Up Techniques in Program Derivation (Q5743597) (← links)
- (Q5875432) (← links)
- Making higher-order superposition work (Q5918575) (← links)
