Proving partial order properties

A temporal verification method which is based upon partial order semantics of traces (Mazurkiewicz, 1987) is presented. The semantic model used here can express the distributed aspects of a program, e. g. properties such as serializability of database transactions, layering of a program, snapshots or the parallel execution of program segments. The proof rules are shown to be sound and relatively complete.

Authors

• Doron Peled
• Amir Pnueli

Keywords

No keywords are indexed for this paper.