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?)
• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• 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
• 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
• Implementing geometric algebra products with binary trees
• Making higher-order superposition work
• Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
• Proving reachability-logic formulas incrementally
• 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
• 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)
• Why3 -- where programs meet provers
• Hammer for Coq: automation for dependent type theory
• Invariants synthesis over a combined domain for automated program verification
• 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
• An assertional proof of the stability and correctness of Natural Mergesort

This page was built for software: WhyML