Name
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 ofMPLS (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-theart 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1007/978-3-030-88885-5_12 | AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2021 |
DocType | Volume | ISSN |
Conference | 12971 | 0302-9743 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Peter Gjøl Jensen | 1 | 32 | 9.38 |
| Stefan Schmid | 2 | 559 | 71.98 |
| Morten Konggaard Schou | 3 | 3 | 0.71 |
| Jirí Srba | 4 | 252 | 28.68 |
| Juan Martin Vanerio | 5 | 13 | 2.58 |
| Ingo van Duijn | 6 | 0 | 1.01 |