• People
• Events
• Research

Proving total correctness of concurrent programs without using auxiliary variables

Abstract: Auxiliary variables or location predicates are commonly used in assertional proof systems for concurrency in order to achieve completeness. When encoded in assertions the references to control flow become entangled in state predicates and can obscure the clarity of argument. We present assertional proof techniques for showing partial correctness, deadlock freedom and termination in which program locations do not need to be encoded in assertions. Instead, the separated reasoning on the flow of control becomes a mechanizable step of the proof. The proposed proof techniques are shown to be sound and complete. Our methodology is applicable to concurrent programming languages based on shared variables or message passing.

LFCS report ECS-LFCS-89-100