TY - GEN
T1 - Producing all ideals of a forest, formally (verification pearl)
AU - Filliâtre, Jean Christophe
AU - Pereira, Mário
N1 - Publisher Copyright:
© Springer International Publishing AG 2016.
PY - 2016/1/1
Y1 - 2016/1/1
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84996879755
U2 - 10.1007/978-3-319-48869-1_4
DO - 10.1007/978-3-319-48869-1_4
M3 - Conference contribution
AN - SCOPUS:84996879755
SN - 9783319488684
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 46
EP - 55
BT - Verified Software
A2 - Blazy, Sandrine
A2 - Chechik, Marsha
PB - Springer Verlag
T2 - 8th International Conference on Verified Software: Theories, Tool and Experiments, VSTTE 2016
Y2 - 17 July 2016 through 18 July 2016
ER -