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] RR-7780, INRIA. 2011, pp.33
Liste complète des métadonnées

https://hal.inria.fr/inria-00636083
Contributor : Claude Marché <>
Submitted on : Wednesday, October 26, 2011 - 4:33:18 PM
Last modification on : Thursday, February 9, 2017 - 3:58:27 PM
Document(s) archivé(s) le : Thursday, November 15, 2012 - 10:36:03 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00636083, version 1

Citation

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

Share

Metrics

Record views

733

Document downloads

441