WhyML

swMATH9709MaRDI QIDQ21688FDOQ21688

Author name not available (Why is that?)

Official website: http://why3.lri.fr/doc-0.80/manual004.html

Cited In (91)

• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• A formally proved, complete algorithm for path resolution with symbolic links
• Assumption propagation through annotated programs
• A Why3 proof of GMP algorithms
• 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
• Verifying Whiley programs with Boogie
• SableJBDD
• 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
• checkbashisms
• BDD
• JDD
• WhyMP, a formally verified arbitrary-precision integer library
• Contract-based verification of MATLAB-style matrix programs
• Tests and proofs for custom data generators
• 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
• 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
• 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
• 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 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