Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Binary Heaps in Why3

This is a Why3 version of the Binary Heaps example, from the VACID-0 benchmarks.

Authors: Claude Marché / Asma Tafat

Topics: Array Data Structure / Tree Data Structure / Permutation

Tools: Why3 / Coq

References: The VACID-0 Benchmarks


The source code is too large to be given on a single page.

The code, its specification and the proofs are presented on the following research report:
Asma Tafat and Claude Marché. Binary heaps formally verified in why3. Research Report 7780, INRIA, October 2011.

The annotated code, the Why3 proof session file and the Coq proof script are available in the archive below.

download ZIP archive