PV3 TIROSchecks user-specified queries for AWS-based networks

Reachability analysis for AWS-based networks

Application domain/field

Type of tool

Reachability checker

Expected input


Uses Soufflé, MonoSAT and Vampire. Should be able to answer queries such as "list all open paths from the Internet to any instance in the VPC (Virtual Private Cloud)"


Used by Amazon Web Services (AWS). It encodes the semantics of the entire AWS cloud network service stack. It has been made to scale well to networks of hundreds of thousands of instances, routers and firewall rules.
Computer network

Related papers

Reachability Analysis for AWS-Based Networks (CAV '19)

Last publication date

12 July 2019

Related tools

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.