How to cook a temporal proof system for your pet language

Published 1 January 1983

Zohar Manna, Amir Pnueli

Citations219

TL;DR

An abstract temporal proof system is presented whose program-dependent part has a high-level interface with the programming language actually studied, and is shown to be relatively complete with respect to pure first-order temporal logic.

Abstract

An abstract temporal proof system is presented whose program-dependent part has a high-level interface with the programming language actually studied. Given a new language, it is sufficient to deline the interface notions of atomic transitions, justice, and fairness in order to obtain a full temporal proof system for this language. This construction is particularly useful for the analysis of concurrent systems. We illustrate the construction on the shared-variable model and on CSP. The generic proof system is shown to be relatively complete with respect to pure first-order temporal logic.

Keywords

Computer Science

Communications of the ACMCommunicating sequential processes

3,789 Citations1983C. A. R. Hoare

View PDF

Theoretical Computer ScienceThe temporal semantics of concurrent programs

701 Citations1981Amir Pnueli

It is demonstrated that specification of the Temporal character of the program's behavior is absolutely essential for the unambiguous understanding of the meaning of programming constructs.

ACM Transactions on Programming Languages and SystemsProving Liveness Properties of Concurrent Programs

583 Citations1982Susan Owicki, Leslie Lamport

A formal proof method, based on temporal logic, for deriving liveness properties is presented, which allows a rigorous formulation of simple informal arguments and how to reason with temporal logic and use safety (invariance) properties in proving liveness is shown.

View PDF

Verification of Concurrent Programs. Part I. The Temporal Framework,

323 Citations1981Zohar Manna, Amir Pnueli

The temporal formalism is introduced as a tool for reasoning about sequences of states and the set of interesting properties is classified into invariance (safety), eventuality (liveness, and precedence) properties.

Lecture notes in computer scienceVerification of concurrent programs: Temporal proof principles

90 Citations2005Zohar Manna, Amir Pnueli

This paper presents proof methods for establishing invariance (safety) and eventuality (liveness) properties of temporal logic in concurrent programs.

International Conference on Distributed Computing SystemsTemporal Logic Specification of Distributed Systems.

59 Citations1981Richard L. Schwartz, P. M. Melliar‐Smith

In selected patients with locally advanced LSCC, VATS played a positive role in postoperative recovery and associated similar survival outcome compared with thoracotomy after neoadjuvant chemotherapy.

Rendezvous with ADA

16 Citations1982Amir Pnueli, W.P. deRoever

A fragment of ADA abstracting the communication and synchronization part is studied, emphasizing the justice and fairness aspects of the selection mechanisms.