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.
Original language | English |
---|---|
Title of host publication | Automated Technology for Verification and Analysis : 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings |
Editors | Zhe Hou, Vijay Ganesh |
Number of pages | 17 |
Publisher | Springer |
Publication date | 2021 |
Pages | 170-186 |
ISBN (Print) | 978-3-030-88884-8 |
ISBN (Electronic) | 978-3-030-88885-5 |
DOIs | |
Publication status | Published - 2021 |
Event | 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 - Virtual, Online Duration: 18 Oct 2021 → 22 Oct 2021 |
Conference
Conference | 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 |
---|---|
City | Virtual, Online |
Period | 18/10/2021 → 22/10/2021 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 12971 LNCS |
ISSN | 0302-9743 |
Bibliographical note
Publisher Copyright:© 2021, Springer Nature Switzerland AG.