Differential Testing of Pushdown Reachability with a Formally Verified Oracle
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
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 |
Publisher | TU Wien Academic Press |
Publication date | 2022 |
Pages | 369-379 |
ISBN (Electronic) | 9783854480532 |
DOIs | |
Publication status | Published - 2022 |
Event | 22nd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2022 - Trento, Italy Duration: 17 Oct 2022 → 21 Oct 2022 |
Conference
Conference | 22nd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2022 |
---|---|
Land | Italy |
By | Trento |
Periode | 17/10/2022 → 21/10/2022 |
Bibliographical note
Publisher Copyright:
© 2022 FMCAD Association and authors.
Links
- https://library.oapen.org/handle/20.500.12657/58896
Final published version
ID: 339333121