Differential Testing of Pushdown Reachability with a Formally Verified Oracle
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
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.
Originalsprog | Engelsk |
---|---|
Titel | Proceedings of the 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022 |
Redaktører | Alberto Griggio, Neha Rungta |
Forlag | TU Wien Academic Press |
Publikationsdato | 2022 |
Sider | 369-379 |
ISBN (Elektronisk) | 9783854480532 |
DOI | |
Status | Udgivet - 2022 |
Begivenhed | 22nd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2022 - Trento, Italien Varighed: 17 okt. 2022 → 21 okt. 2022 |
Konference
Konference | 22nd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2022 |
---|---|
Land | Italien |
By | Trento |
Periode | 17/10/2022 → 21/10/2022 |
Bibliografisk note
Funding Information:
This research was supported by the Independent Research Fund Denmark (DFF project QASNET) and by Novo Nordisk Fonden (NNF20OC0063462).
Publisher Copyright:
© 2022 FMCAD Association and authors.
Links
- https://library.oapen.org/handle/20.500.12657/58896
Forlagets udgivne version
ID: 339333121