Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Binary Heaps Formally Verified in Why3

Asma Tafat 1 Claude Marché 1, 2 
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : The VACID-0 benchmarks is a set of small programs which pose challenges for formal verification of their functional behavior. This paper reports on the formal verification of one of these challenges: binary heaps. The solution given here is performed using the Why3 environment for program verification. The expected behavior of the program is specified in Why3 logic, structured using the constructs for building hierarchies of theories provided by Why3. The proofs are achieved by a significant amount of automation, using SMT solvers for a large majority of the verification conditions generated, whereas the remaining verification conditions are discharged by interactive constructions of proof scripts using the Coq proof assistant. The general aim of this case study is to demonstrate the usability and efficiency of both the Why3 specification language and the accompanying tools, which offer a fairly advanced environment for specification while keeping a significant amount of automation of proofs.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Wednesday, October 26, 2011 - 4:33:18 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:07 AM
Long-term archiving on: : Thursday, November 15, 2012 - 10:36:03 AM


Files produced by the author(s)


  • HAL Id : inria-00636083, version 1


Asma Tafat, Claude Marché. Binary Heaps Formally Verified in Why3. [Research Report] RR-7780, INRIA. 2011, pp.33. ⟨inria-00636083⟩



Record views


Files downloads