Skip to Main content Skip to Navigation
Conference papers

Producing All Ideals of a Forest, Formally (Verification Pearl)

Abstract : In this paper we present the first formal proof of an implementation of Koda and Ruskey's algorithm, an algorithm for generating all ideals of a forest poset as a Gray code. One contribution of this work is to exhibit the invariants of this algorithm, which proved to be challenging. We implemented, specified, and proved this algorithm using the Why3 tool. This allowed us to employ a combination of several automated theorem provers to discharge most of the verification conditions, and the Coq proof assistant for the remaining two.
Document type :
Conference papers
Complete list of metadatas

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/hal-01316859
Contributor : Mário José Parreira Pereira <>
Submitted on : Tuesday, November 29, 2016 - 2:21:58 PM
Last modification on : Tuesday, April 21, 2020 - 1:12:38 AM
Document(s) archivé(s) le : Monday, March 27, 2017 - 8:32:12 AM

File

paper_6.pdf
Files produced by the author(s)

Identifiers

Citation

Jean-Christophe Filliâtre, Mário Pereira. Producing All Ideals of a Forest, Formally (Verification Pearl). VSTTE 2016, Jul 2016, Toronto, Canada. pp.46 - 55, ⟨10.1007/978-3-319-48869-1_4⟩. ⟨hal-01316859v2⟩

Share

Metrics

Record views

427

Files downloads

412