Differential Testing of Pushdown Reachability with a Formally Verified Oracle
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Standard
Differential Testing of Pushdown Reachability with a Formally Verified Oracle. / Schlichtkrull, Anders; Schou, Morten Konggaard; Srba, Jiří; Traytel, Dmitriy.
Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022. red. / Alberto Griggio; Neha Rungta. TU Wien Academic Press, 2022. s. 369-379.Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Differential Testing of Pushdown Reachability with a Formally Verified Oracle
AU - Schlichtkrull, Anders
AU - Schou, Morten Konggaard
AU - Srba, Jiří
AU - Traytel, Dmitriy
N1 - Publisher Copyright: © 2022 FMCAD Association and authors.
PY - 2022
Y1 - 2022
N2 - Pushdown automata are an essential model of recursive computation. In model checking and static analysis, numerous problems can be reduced to reachability questions about pushdown automata and several efficient libraries implement automata-theoretic algorithms for answering these questions. These libraries are often used as core components in other tools, and therefore it is instrumental that the used algorithms and their implementations are correct. We present a method that significantly increases the trust in the answers provided by the libraries for pushdown reachability by (i) formally verifying the correctness of the used algorithms using the Isabelle/HOL proof assistant, (ii) extracting executable programs from the formalization, (iii) implementing a framework for the differential testing of library implementations with the verified extracted algorithms as oracles, and (iv) automatically minimizing counter-examples from the differential testing based on the delta-debugging methodology. We instantiate our method to the concrete case of PDAAAL, a state-of-the-art library for pushdown reachability. Thereby, we discover and resolve several nontrivial errors in PDAAAL.
AB - Pushdown automata are an essential model of recursive computation. In model checking and static analysis, numerous problems can be reduced to reachability questions about pushdown automata and several efficient libraries implement automata-theoretic algorithms for answering these questions. These libraries are often used as core components in other tools, and therefore it is instrumental that the used algorithms and their implementations are correct. We present a method that significantly increases the trust in the answers provided by the libraries for pushdown reachability by (i) formally verifying the correctness of the used algorithms using the Isabelle/HOL proof assistant, (ii) extracting executable programs from the formalization, (iii) implementing a framework for the differential testing of library implementations with the verified extracted algorithms as oracles, and (iv) automatically minimizing counter-examples from the differential testing based on the delta-debugging methodology. We instantiate our method to the concrete case of PDAAAL, a state-of-the-art library for pushdown reachability. Thereby, we discover and resolve several nontrivial errors in PDAAAL.
UR - http://www.scopus.com/inward/record.url?scp=85148085838&partnerID=8YFLogxK
U2 - 10.34727/2022/isbn.978-3-85448-053-2-44
DO - 10.34727/2022/isbn.978-3-85448-053-2-44
M3 - Article in proceedings
AN - SCOPUS:85148085838
SP - 369
EP - 379
BT - Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022
A2 - Griggio, Alberto
A2 - Rungta, Neha
PB - TU Wien Academic Press
T2 - 22nd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2022
Y2 - 17 October 2022 through 21 October 2022
ER -
ID: 339333121