Issue No. 09 - September (1990 vol. 16)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.58786
<p>How a mechanized tool for reasoning about CSP (communicating sequential processes) can be developed by customizing an existing general-purpose theorem prover based on higher-order logic is described. How the trace semantics of CSP operators can be mechanized in higher-order logic is investigated, and how the laws associated with these operators can be proved from their semantic definitions is shown. The resulting system is one in which natural-deduction style proofs can be conducted using the standard CSP laws.</p>
mechanising CSP trace theory; higher order logic; communicating sequential processes; general-purpose theorem prover; formal logic; formal specification; theorem proving.
A. Camilleri, "Mechanizing CSP Trace Theory in Higher Order Logic," in IEEE Transactions on Software Engineering, vol. 16, no. , pp. 993-1004, 1990.