A structural embedding of Ocsid in PVS. (English) Zbl 1005.68532

Kellomäki, Pertti

Boulton, Richard J. (ed.) et al., Theorem proving in higher order logics. 14th international conference, TPHOLs 2001, Edinburgh, Scotland, GB, September 3-6, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2152, 281-296 (2001).

Summary: We describe a structural embedding of the Ocsid specification language into the logic of the PVS theorem prover. A front end tool is used to manipulate the structural elements of the language, while the expression language is directly borrowed from the theorem prover.
The structural embedding allows us to express and verify invariant properties of distributed systems in an abstract form. An invariant can be verified once, and reused multiple times by discharging a set of relatively simple proof obligations.
For the entire collection see [Zbl 0971.00027].

MSC:

68T15

Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

HOL; DisCo; Coq; HOL-UNITY; PVS; Ocsid