A Front-End Generator for Verification Tools
Rance Cleaveland
Eric Madelaine
Steve Sims
In TACAS, pages
201--215
Abstract:
This paper describes the Process Algebra Compiler (PAC), a
front-end generator for process-algebra-based verification tools. Given
descriptions of a process algebra's concrete and abstract syntax and
semantics as structural operational rules, the PAC produces syntactic
routines and functions for computing the semantics of programs in the
algebra. Using this tool greatly simplifies the task of adapting verification
tools to the analysis of systems described in different languages; it may
therefore be used to achieve source-level compatibility between different
verification tools. Although the initial verification tools targeted by the
PAC are MAUTO and the Concurrency Workbench, the structure of the PAC caters
for the support of other tools as well.
Comments
N.C. State University, U.S.A., INRIA, Antibes, Franc.
Available as PostScript,
DVI.
![[BRICS symbol]](http://www.brics.aau.dk/BRICS/GIF/BRICS/msymbol8mm.GIF)
BRICS WWW home page