WhyML

swMATH9709MaRDI QIDQ21688FDOQ21688

Author name not available (Why is that?)

Cited In (35)

• 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
• Title not available (Why is that?)
• Combining Top-Down and Bottom-Up Techniques in Program Derivation
• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• Invariants Synthesis over a Combined Domain for Automated Program Verification
• WhyMP, a formally verified arbitrary-precision integer library
• Contract-based verification of MATLAB-style matrix programs
• Tests and proofs for custom data generators
• Assumption propagation through annotated programs
• Building program construction and verification tools from algebraic principles
• A Generic Intermediate Representation for Verification Condition Generation
• 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
• Implementing geometric algebra products with binary trees
• Why3 — Where Programs Meet Provers
• Making higher-order superposition work
• An Assertional Proof of the Stability and Correctness of Natural Mergesort
• Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• A generic framework for symbolic execution: a coinductive approach
• Title not available (Why is that?)
• A verification-driven framework for iterative design of controllers
• A formally verified interpreter for a shell-like programming language
• The matrix reproved (verification pearl)
• Proving Reachability-Logic Formulas Incrementally
• Hammer for Coq: automation for dependent type theory
• Relational cost analysis in a functional-imperative setting
• Title not available (Why is that?)
• The spirit of ghost code
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Modular Verification of Higher-Order Functional Programs

This page was built for software: WhyML