A stuttering closed temporal logic for modular reasoning about concurrent programs

1. M. Abadi and L. Lamport. The existence of refinement mappings. In Third Annual Symposium on Logic In Computer Science, pages 165–177, Edinburgh, July 1988.

   Google Scholar 

2. M. Abadi and L. Lamport. Composing specifications. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Springer Verlag, 1990. LNCS 430.

   Google Scholar 

3. H. Barringer. The use of temporal logic in the compositional specification of concurrent systems. In A. Galton, editor, Temporal logics and their applications, pages 53–90, London, 1987. Academic Press.

   Google Scholar 

4. H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In Sixteenth ACM Symposium on Theory of Computing, pages 51–63, April 1984. ACM.

   Google Scholar 

5. L. Lamport. The ‘Hoare Logic’ of concurrent programs. Acta Informatica, 14:21–37, 1980.

   Article  Google Scholar 

6. L. Lamport. Specifying concurrent program modules. ACM Transactions On Programming Languages And Systems, 2(5):190–222, april 1983.

   Article  Google Scholar 

7. L. Lamport. What good is temporal logic? pages 657–677. IFIP, 1983.

   Google Scholar 

8. L. Lamport. A simple approach to specifying concurrent systems. Communications of ACM, 1(32):32–45, January 1989.

   Article  Google Scholar 

9. L. Lamport. The temporal logic of actions. Technical report, DEC Palo Alto, December 1991.

   Google Scholar 

10. L. Abadi and G.D. Plotkin A logical view of composition. Technical report, DEC Palo Alto, May 1, 1992.

    Google Scholar 

11. O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Logics of Programs, pages 196–218. Spinger Verlag, 1985. LNCS 193.

    Google Scholar 

12. Z. Manna and A. Pnueli. The anchored version of teh temporal framework. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, pages 201–284, New York, 1981. Spinger Verlag. LNCS 354.

    Google Scholar 

13. A. Pnueli. System Specification and Refinement in Temporal Logic. In LNCS, 1992. Spinger Verlag.

    Google Scholar 

14. Z. Manna and A. Pnueli. Verification of concurrent programs: A temporal proof system. In 4th School on Advanced Programming, pages 163–255, June 1982.

    Google Scholar 

15. Z. Manna and A. Pnueli. The modal logic of programs. Lecture Notes in Computer Science 71, pages 257–289, 1979.

    Google Scholar 

16. Z. Manna and A. Pnueli. Verification of concurrent programs: The temporal frame-work. In R.S. Boyer and J.S. Moore, editors, Correctness Problem in Computer science, pages 215–273, London, 1982. Academic Press.

    Google Scholar 

17. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991. ISBN 0-387-97664-7.

    Google Scholar 

18. Z. Manna and A. Pnueli. Verification of concurrent programs: A temporal proof system. In 4^th School on Advanced Programming, pages 163–255, June 1982.

    Google Scholar 

19. Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In Proceedings of the Symposium on Principles of Programming Languages, 1983.

    Google Scholar 

20. D. Méry and A. Mokkedem. A proof environment for a subset of SDL. In O. Faergemand and R. Reed, editors, Fifth SDL Forum Evolving methods. North-Holland, 1991.

    Google Scholar 

21. D. Méry and A. Mokkedem. Crocos: An integrated environment for interactive verification of SDL specifications. In G. Bochmann, editor, Computer-Aided Verification Proceedings. Springer Verlag, 1992.

    Google Scholar 

22. A. Mokkedem and D. Méry. On using a Composition Principle to Design Parallel Programs. In Third International Conference on Algebraic Methodology and Software Technology proceedings, AMAST'93, June 21–25, 1993, University of Twente, The Netherlands.

    Google Scholar 

23. A. Mokkedem and D. Méry. On using temporal logic for refinement and compositional verification of concurrent systems. Technical Report 93-R-324, CRIN, 1993.

    Google Scholar 

24. A. Mokkedem and D. Méry. A Stuttering Closed Temporal Logic for Modular Reasoning about Concurrent Programs. Technical Report, CRIN, 1994.

    Google Scholar 

25. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319–340, 1976.

    Article  Google Scholar 

26. L. Paulson and T. Nipkow. Isabelle tutorial and users's manual. Technical report, University of Cambridge, Computer Laboratory, 1990.

    Google Scholar 

27. K. Gödel. Über Formal Unentscheidbare Sätze der Principa Mathematica under Verwandeter Systeme, I Monatshefte für Mathematic und Physik, 38, 1931.

    Google Scholar 

28. J. Zwiers and W.P. de Roever. Predicates are predicate transformers: a unified compositional theory for concurrency. Communications of ACM, 265–279, 1989.

    Google Scholar 

Download references