PAM is able to compute the abstract state space for user-provided predicates in Murphi models, i.e. to check the reachability of each predicate property. It is an over-approximation based abstraction. The algorithms we use are based on Satyaki Das's PhD thesis. It uses CVC Lite as the decision procedure. For major details, please see our technical report.
PAM1.0 can be downloaded from here(.tar.gz).
School of Computing * 50 S. Central Campus Dr. Rm. 3190 * Salt Lake
City, UT 84112
801-585-3866 * Send comments to xiachen AT cs.utah.edu