Artifact for Submission 172:

Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers

1. Design Description

An overview of PAT

Architecture

The above figure demonstrates the architecture of our tool. It contains two components: PAT and QuTL MCer.

Usage: To use our tool, the users first need to compile a P program, which is done via P compiler (See tutorial and Section 6 of the paper for more details). Then, our tool will run the verification on the compiled P program. Our tool provides rich features to perform verification. Two main features are presented as follows:

The two features can be used simultanously.

2. Programmer's Guide

See here for the off-the-shelf programmer's guide in html format.

We included a SandCastle project in directory doc/ to help users (re-)generate the programmer's guide with SandCastle help file builder.