Faster Pushdown Reachability Analysis with Applications in Network Verification

Peter Gjøl Jensen, Stefan Schmid, Morten Konggaard Schou, Jiří Srba*, Juan Vanerio, Ingo van Duijn

*Corresponding author for this work

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

3 Citations (Scopus)

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 languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis : 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021, Proceedings
EditorsZhe Hou, Vijay Ganesh
Number of pages17
PublisherSpringer
Publication date2021
Pages170-186
ISBN (Print)978-3-030-88884-8
ISBN (Electronic)978-3-030-88885-5
DOIs
Publication statusPublished - 2021
Event19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 - Virtual, Online
Duration: 18 Oct 202122 Oct 2021

Conference

Conference19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021
CityVirtual, Online
Period18/10/202122/10/2021
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12971 LNCS
ISSN0302-9743

Bibliographical note

Publisher Copyright:
© 2021, Springer Nature Switzerland AG.

Fingerprint

Dive into the research topics of 'Faster Pushdown Reachability Analysis with Applications in Network Verification'. Together they form a unique fingerprint.

Cite this