WhyML

swMATH9709MaRDI QIDQ21688

No author found.

Related Items (35)

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

This page was built for software: WhyML