Trace-based network proof systems

1 May 1992

journal article
Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems

Vol. 14 (3) , 396-416
https://doi.org/10.1145/129393.129396

Abstract

We consider incomplete trace-based network proof systems for safety properties, identifying extensions that are necessary and sufficient to achieve relative completeness. We investigate the expressiveness required of any trace logic to encode these extensions.

Keywords

This publication has 7 references indexed in Scilit:

A model and temporal proof system for networks of processes
Distributed Computing, 1986
The incompleteness of Misra and Chandy's proof systems
Information Processing Letters, 1985
A semantics and proof system for communicating processes
Lecture Notes in Computer Science, 1984
A more complete model of communicating processes
Theoretical Computer Science, 1983
Ten Years of Hoare's Logic: A Survey—Part I
ACM Transactions on Programming Languages and Systems, 1981
Scenarios: A model of non-determinate computation
Published by Springer Nature ,1981
Proving the Correctness of Multiprocess Programs
IEEE Transactions on Software Engineering, 1977