Abstract
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.
Original language | English |
---|---|
Title of host publication | Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design – FMCAD 2022 |
Editors | Alberto Griggio, Neha Rungta |
Number of pages | 11 |
Volume | 3 |
Publisher | TU Wien Academic Press |
Publication date | Oct 2022 |
Pages | 369-379 |
Chapter | 44 |
ISBN (Electronic) | 978-3-85448-053-2 |
DOIs | |
Publication status | Published - Oct 2022 |
Event | Formal Methods in Computer-Aided Design 2022 - Trento, Italy Duration: 17 Oct 2022 → 21 Oct 2022 |
Conference
Conference | Formal Methods in Computer-Aided Design 2022 |
---|---|
Country/Territory | Italy |
City | Trento |
Period | 17/10/2022 → 21/10/2022 |
Series | Conference Series: Formal Methods in Computer-Aided Design |
---|
Fingerprint
Dive into the research topics of 'Differential Testing of Pushdown Reachability with a Formally Verified Oracle'. Together they form a unique fingerprint.Datasets
-
Repeatability Package for "Differential Testing of Pushdown Reachability with a Formally Verified Oracle"
Schlichtkrull, A. (Creator), Schou, M. K. (Creator), Srba, J. (Creator) & Traytel, D. (Creator), Zenodo, 2 Aug 2022
DOI: 10.5281/zenodo.6952979, https://zenodo.org/record/6952979
Dataset