EECS 298-11: CAD Seminar Monday, May 5, 1997, 3pm ^^^^^^ ^^^ Cory Hall--Hogan Room Using Partial Orders to Verify Concurrent Systems Shmuel Katz Computer Science Department The Technion--Israel Institute of Technology An approach to justifying the correctness of concurrent systems will be presented. In this approach, a proof is divided into two independent stages. In the first stage, a subclass of the computations are identified as the Convenient ones and are proven to satisfy the specification. Then in the second stage, all other computations are shown to be equivalent to one of the convenient ones. The equivalence maintains the ordering of all causally dependent events, but allows independent events to occur in different orders. The equivalence must also be shown to respect the specification. This stage could be considered as a `loosening' of the ordering imposed by the convenient executions. The advantage of this separation is that different kinds of reasoning and induction can be used for the two aspects. The convenient computations can be chosen so that their verification is relatively simple. A proof rule with well-founded sets is proposed for the proofs of equivalence.