Why3 - Where Programs Meet Provers

By Jean-Christophe Filliâtre, A. Paskevich. European Symposium on Programming, 2013

635 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Signal Processing

View Paper: https://www.semanticscholar.org/paper/4d011ed17687648ac4ce719e24c3bab77a4a143e

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Signal Processing

Citations in the corpus

Formal Verification of Smart Contracts: Short Paper (2016, methodology): “In parallel with this work, Luu et al. [6] use symbolic execution to detect ﬂaws in EVM bytecode programs, and an experimental Why3 [5] formal veriﬁcation backend is now available from the Solidity web IDE [4].”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, background): “…are widely recognized as crucial back-end reasoning engines for a variety of applications, including software and hardware veriﬁcation [19, 52, 60, 68, 82, 86], model checking [41, 42, 98], type checking, static analysis, security [10,62], automated test-case generation [40,135], synthesis…”
ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection (2018, methodology): “Fillâtre [6] presented Why3, a tool used for program verification, which is now available within Solidity Web IDE [9] as the formal verification backend.”
KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (2018, methodology): “For example, the Solidity IDE incorporates Why3 [41] (a semi-automated theorem prover) to help verify smart contracts written in the higher-level Solidity language.”
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale (2018, methodology): “[38], Idris [39], and Why3 [40, 41], followed by subsequent mechanised contract verification efforts.”
Smart Contract Development: Challenges and Opportunities (2021, methodology): “To prove the correctness of smart contracts, some researchers proposed to use formal verification methods to perform complete analysis of smart contracts by using interactive theorem provers [13], [61], [14], [109], [4], such as Isabelle/HOL29, F*30, Why3 [42], and K31, etc.”
Under-optimized smart contracts devour your money (2017, background): “Bhargavan et al. use formal veriﬁcation to analyze smart contracts (e.g., whether contracts check the return value of a send operation because send may fail) [10], [11].”
Dependent types and multi-monadic effects in F* (2016, neutral): “Finally, we prove that we return the current entry in the reader’s current position in the log and then advance the position, except if there are no more entries or if the cipher is incorrect.”