Using branching time temporal logic to synthesize synchronization skeletons

Science of Computer Programming - Tập 2 Số 3 - Trang 241-266 - 1982
E. Allen Emerson1, Edmund M. Clarke2
1Computer Sciences Department, University of Texas at Austin, Austin, TX 78712, U.S.A.
2Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213, U.S.A.

Tóm tắt

Từ khóa


Tài liệu tham khảo

Ben-Ari, 1981, Personal Communication

Ben-Ari, 1981, Finite models for deterministic propositional dynamic logic, Proc. 8th International Colloquium on Automata, Languages, and Programming, 249

Ben-Ari, 1981, The temporal logic of branching time, Proc. 8th Annual ACM Symposium on Principles of Programming Languages, 164

Clarke, 1981, Design and synthesis of synchronization skeletons using branching time temporal logic (Abridged version), 131, 52

Clarke, 1983, Automatic verification of finite state concurrent systems: A practical approach, 10th Annual ACM Symposium on Principles of Programming Languages

E.M. Clarke, Program invariants as fixpoints, Computing 21 (4) 273-294.

Emerson, 1981, Branching time temporal logic and the design of correct concurrent programs

Emerson, 1980, Characterizing correctness properties of parallel programs as fixpoints, 85, 169

Emerson, 1982, Decision procedures and expressiveness in the temporal logic of branching time, Proc. 14th Annual ACM Symposium on Theory of Computing, 169

Flon, 1981, The total correctness of parallel programs, SIAM J. Comput., 227, 10.1137/0210016

Gabbay, 1980, The temporal analysis of fairness, Proc. 7th Annual ACM Symposium on Principles of Programming Languages, 163

Hughes, 1968

Lamport, 1980, ‘Sometimes’ is sometimes ‘not never’, Proc. 7th Annual ACM Symposium on Principles of Programming Languages, 174

Laventhal, 1978, Synthesis of synchronization code for data abstractions

Manna, 1981, Synthesis of communicating processes from temporal logic specifications, 131, 253

S. Owicki and L. Lamport, Proving liveness properties of concurrent programs, ACM Trans. Programming Languages 4 (3) 455-495.

Pnueli, 1981, The temporal semantics of concurrent programs, Theoret. Comput. Sci., 13, 45, 10.1016/0304-3975(81)90110-9

Pratt, 1980, A near optimal method for reasoning about action, J. Comput. Systems Sci., 20, 231, 10.1016/0022-0000(80)90061-6

Ramamritham, 1980, Specification and synthesis of synchronizers, Proc. 9th International Conference on Parallel Processing, 311

Smullyan, 1968

Tarski, 1955, A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 5, 285, 10.2140/pjm.1955.5.285

Wolper, 1981, Temporal logic can be more expressive, Proc. 22nd Annual Symposium on Foundations of Computer Science, 340, 10.1109/SFCS.1981.44

Wolper, 1982, Specification and synthesis of communicating processes using an extended temporal logic (Preliminary version), Proc. 9th Annual ACM Symposium on Principles of Programming Languages, 20