Abstract
A description of a tool to support computer-aided construction of proofs for parallel systems is given. In contrast to the conventional approach based on state space exploration, we use an axiomatic approach. The axioms we use for the construction of proofs, are based on ACP. Besides these standard axioms we also consider tactics for shortening proofs. We use PSF (Process Specification Formalism), an extension of ACP with abstract data types, to describe the processes subject to the verification.
Cite
CITATION STYLE
Mauw, S., & Veltink, G. J. (1992). A proof assistant for PSF. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 575 LNCS, pp. 158–168). Springer Verlag. https://doi.org/10.1007/3-540-55179-4_16
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
