Abstract
Reachability analysis of pushdown systems is a fundamental problem in model checking that comes with a wide range of applications. We study performance improvements of pushdown reachability analysis and as a case study, we consider the verification of the policy-compliance of MPLS (Multiprotocol Label Switching) networks, an application domain that has recently received much attention. Our main contribution are three techniques that allow us to speed up the state-of-the-art pushdown reachability tools by an order of magnitude. These techniques include the combination of classic pre∗ and post∗ saturation algorithms into a dual-search algorithm, an on-the-fly technique for detecting the possibility of early termination, as well as a counter-example guided abstraction refinement technique that improves the performance in particular for the negative instances where the early termination technique is not applicable. As a second contribution, we describe an improved translation of MPLS networks to pushdown systems and demonstrate on an extensive set of benchmarks of real internet wide-area networks the efficiency of our approach.
Originalsprog | Engelsk |
---|---|
Titel | Automated Technology for Verification and Analysis : 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings |
Redaktører | Zhe Hou, Vijay Ganesh |
Antal sider | 17 |
Forlag | Springer |
Publikationsdato | 2021 |
Sider | 170-186 |
ISBN (Trykt) | 978-3-030-88884-8 |
ISBN (Elektronisk) | 978-3-030-88885-5 |
DOI | |
Status | Udgivet - 2021 |
Begivenhed | 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 - Virtual, Online Varighed: 18 okt. 2021 → 22 okt. 2021 |
Konference
Konference | 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 |
---|---|
By | Virtual, Online |
Periode | 18/10/2021 → 22/10/2021 |
Navn | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Vol/bind | 12971 LNCS |
ISSN | 0302-9743 |
Bibliografisk note
Funding Information:Research supported by the Vienna Science and Technology Fund (WWTF), ICT19-045 (WHATIF), and the DFF project QASNET.
Publisher Copyright:
© 2021, Springer Nature Switzerland AG.