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 metadata

Cited literature [6 references]  Display  Hide  Download
Contributor : Mário José Parreira Pereira Connect in order to contact the contributor
Submitted on : Tuesday, November 29, 2016 - 2:21:58 PM
Last modification on : Saturday, June 25, 2022 - 10:22:37 PM
Long-term archiving on: : Monday, March 27, 2017 - 8:32:12 AM


Files produced by the author(s)



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⟩



Record views


Files downloads