How to use the scripts
Public and private server A system consisting of public and private servers. The system can generate an unlimited number of public servers and one private server. All servers are connected to each other.	Literature (p.43), short introduction (p.19). SourceXML Visualisation Scripts
Public and private server 2 A modified version of the previous example. The abstraction refinement module (abstref) is needed for successful verification.	Literature (p.3), SourceXML Visualisation Scripts
Dining philosophers (finite-state version) A finite-state system of dining philosophers: absence of deadlock states is checked by analyzing cycles in the hypergraph associated with the approximated unfolding.	Literature SourceXML Visualisation Script
Dining philosophers (infinite-state version) The dining philosophers example as given above, but extended to an infinite-state system by adding a rule which allows an eating philosopher to reproduce. This rule creates another hungry philosopher with an adjacent fork.	Literature SourceXML Visualisation Script
Firewall A network of secure and insecure locations, divided by a firewall. Simple distributed system with mobility, consisting of locations (secure and non-secure), processes running on these locations, and connections (secure, non-secure or firewall connections, which can only be crossed in one direction).	Literature SourceXML Visualisation Script
Firewall 2 A modified version of the previous example. The property to be proven is that no process running on a non-secure location can influence a process running on a secure location, which can be formalized as the absence of causal dependencies between such processes. For this example the abstraction refinement module (abstref) should be installed.	Literature SourceXML Visualisation Script
Red-black trees Generate all possible red-black trees (a form of balanced search trees) and model the insertion of elements into red-black trees.	Literature SourceXML Visualisation Script
Red-black trees converted A modified version of the previous example which can be analyzed more easily. Here we use Augur in order to show that the insertion of elements preserves the property that there are no consecutive red nodes in a tree, a requirement for red-black trees.	Literature SourceXML Visualisation Script
External-internal processes A system consisting of public and private servers, internal and external processes. Public servers can extend the network by creating new connections; internal processes can wander around the network. The property to be proven here is that the external process is never connected to a private server and given access to classified data.	Literature SourceXML Visualisation Script
Mutual exclusion A mutual exclusion protocol where a token is passed around. Only the process in possession of the token can use a shared resource.	Literature SourceXML Visualisation Script
Resources A system of several processes sharing two resources. A process needs both resources in order to perform some task.	Literature SourceXML Visualisation Script