Liu, Yu;
Subotic, Pavle;
Letier, Emmanuel;
Mechtaev, Sergey;
Roychoudhury, Abhik;
(2023)
Efficient SMT-Based Network Fault Tolerance Verification.
In: Katoen, JP and Chechik, M and Leucker, M, (eds.)
Formal Methods. FM 2023.
(pp. pp. 92-100).
Springer: Cham, Springer.
Preview |
Text
fm23.pdf - Accepted Version Download (316kB) | Preview |
Abstract
Network control planes are highly sophisticated, resulting in networks that are difficult and error-prone to configure. Although several network verification tools have been developed to assist network operators, they are limited and inefficient in handling fault-tolerance policies. In this paper, we propose a novel SMT encoding to speed up control plane fault tolerance verification by pruning failed topologies. This encoding exploits the observation that the verifier has to check failures only for the links lying on a set of best paths which can be computed by a recursive algorithm. We implemented our technique in Minesweeper, a state-of-the-art SMT-based verifier. Our evaluation shows that the new encoding speeds up verification by the factor of 3.1–26.9X.
| Type: | Proceedings paper |
|---|---|
| Title: | Efficient SMT-Based Network Fault Tolerance Verification |
| ISBN-13: | 978-3-031-27480-0 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-031-27481-7_7 |
| Publisher version: | https://doi.org/10.1007/978-3-031-27481-7_7 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Science & Technology, Technology, Computer Science, Software Engineering, Computer Science, Theory & Methods, Computer Science |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery-pp.ucl.ac.uk/id/eprint/10184109 |
Archive Staff Only
 |
View Item |
