PV1 Origamiverifies reachability in networks in the presence of faults

Application domain/field

Type of tool

Network verification tool

Expected input

? (a network configuration, possibly a source and destination node)

Expected output

Network is verified successfully or a property violation is reported?

Internals

Origami can be used to verify reachability in networks in the presence of faults. Origami first computes a small abstract network that satisfies certain SPPF (Stable Path Problems with Faults) effective approximation conditions. If this abstraction satisfies the desired property then the verification terminates successfully. If it could not be verified, then it checks whether the returned counterexample is an actual counterexample. If not, then a new abstraction is computed. Uses Batfish, Z3.

Comments

The goal of Origami is scalability, they want to be able to analyze large networks (e.g. 1000s of routers).
Computer network

Links

Repository (? linked on author's webpage): https://github.com/NetworkVerification/nv

Related papers

https://doi.org/10.1007/978-3-030-25543-5_18

Last publication date

12 July 2019

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.