? (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).
