{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:20:10Z","timestamp":1725456010154},"publisher-location":"Berlin\/Heidelberg","reference-count":28,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354058241X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0014000","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:34:32Z","timestamp":1132731272000},"page":"382-397","source":"Crossref","is-referenced-by-count":3,"title":["A stuttering closed temporal logic for modular reasoning about concurrent programs"],"prefix":"10.1007","author":[{"given":"Abdelillah","family":"Mokkedem","sequence":"first","affiliation":[]},{"given":"Dominique","family":"M\u00e9ry","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. In Third Annual Symposium on Logic In Computer Science, pages 165\u2013177, Edinburgh, July 1988.","DOI":"10.1109\/LICS.1988.5115"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/3-540-52559-9_59"},{"key":"24_CR3","first-page":"53","volume-title":"Temporal logics and their applications","author":"H. Barringer","year":"1987","unstructured":"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\u201390, London, 1987. Academic Press."},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In Sixteenth ACM Symposium on Theory of Computing, pages 51\u201363, April 1984. ACM.","DOI":"10.1145\/800057.808665"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BF00289062","volume":"14","author":"L. Lamport","year":"1980","unstructured":"L. Lamport. The \u2018Hoare Logic\u2019 of concurrent programs. Acta Informatica, 14:21\u201337, 1980.","journal-title":"Acta Informatica"},{"issue":"5","key":"24_CR6","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"2","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules. ACM Transactions On Programming Languages And Systems, 2(5):190\u2013222, april 1983.","journal-title":"ACM Transactions On Programming Languages And Systems"},{"key":"24_CR7","unstructured":"L. Lamport. What good is temporal logic? pages 657\u2013677. IFIP, 1983."},{"issue":"32","key":"24_CR8","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/63238.63240","volume":"1","author":"L. Lamport","year":"1989","unstructured":"L. Lamport. A simple approach to specifying concurrent systems. Communications of ACM, 1(32):32\u201345, January 1989.","journal-title":"Communications of ACM"},{"key":"24_CR9","unstructured":"L. Lamport. The temporal logic of actions. Technical report, DEC Palo Alto, December 1991."},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"L. Abadi and G.D. Plotkin A logical view of composition. Technical report, DEC Palo Alto, May 1, 1992.","DOI":"10.1016\/0304-3975(93)90151-I"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Logics of Programs, pages 196\u2013218. Spinger Verlag, 1985. LNCS 193.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"24_CR12","series-title":"LNCS 354","first-page":"201","volume-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","author":"Z. Manna","year":"1981","unstructured":"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\u2013284, New York, 1981. Spinger Verlag. LNCS 354."},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"A. Pnueli. System Specification and Refinement in Temporal Logic. In LNCS, 1992. Spinger Verlag.","DOI":"10.1007\/3-540-56287-7_92"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Verification of concurrent programs: A temporal proof system. In 4th School on Advanced Programming, pages 163\u2013255, June 1982.","DOI":"10.21236\/ADA116035"},{"key":"24_CR15","first-page":"257","volume":"71","author":"Z. Manna","year":"1979","unstructured":"Z. Manna and A. Pnueli. The modal logic of programs. Lecture Notes in Computer Science 71, pages 257\u2013289, 1979.","journal-title":"Lecture Notes in Computer Science"},{"key":"24_CR16","first-page":"215","volume-title":"Correctness Problem in Computer science","author":"Z. Manna","year":"1982","unstructured":"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\u2013273, London, 1982. Academic Press."},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991. ISBN 0-387-97664-7.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Verification of concurrent programs: A temporal proof system. In 4 th School on Advanced Programming, pages 163\u2013255, June 1982.","DOI":"10.21236\/ADA116035"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/567067.567082"},{"key":"24_CR20","unstructured":"D. M\u00e9ry 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."},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"D. M\u00e9ry and A. Mokkedem. Crocos: An integrated environment for interactive verification of SDL specifications. In G. Bochmann, editor, Computer-Aided Verification Proceedings. Springer Verlag, 1992.","DOI":"10.1007\/3-540-56496-9_27"},{"key":"24_CR22","volume-title":"On using a Composition Principle to Design Parallel Programs","author":"A. Mokkedem","year":"1993","unstructured":"A. Mokkedem and D. M\u00e9ry. On using a Composition Principle to Design Parallel Programs. In Third International Conference on Algebraic Methodology and Software Technology proceedings, AMAST'93, June 21\u201325, 1993, University of Twente, The Netherlands."},{"key":"24_CR23","unstructured":"A. Mokkedem and D. M\u00e9ry. On using temporal logic for refinement and compositional verification of concurrent systems. Technical Report 93-R-324, CRIN, 1993."},{"key":"24_CR24","unstructured":"A. Mokkedem and D. M\u00e9ry. A Stuttering Closed Temporal Logic for Modular Reasoning about Concurrent Programs. Technical Report, CRIN, 1994."},{"key":"24_CR25","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319\u2013340, 1976.","journal-title":"Acta Informatica"},{"key":"24_CR26","unstructured":"L. Paulson and T. Nipkow. Isabelle tutorial and users's manual. Technical report, University of Cambridge, Computer Laboratory, 1990."},{"key":"24_CR27","doi-asserted-by":"crossref","unstructured":"K. G\u00f6del. \u00dcber Formal Unentscheidbare S\u00e4tze der Principa Mathematica under Verwandeter Systeme, I Monatshefte f\u00fcr Mathematic und Physik, 38, 1931.","DOI":"10.1007\/BF01700692"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"J. Zwiers and W.P. de Roever. Predicates are predicate transformers: a unified compositional theory for concurrency. Communications of ACM, 265\u2013279, 1989.","DOI":"10.1145\/72981.73000"}],"container-title":["Lecture Notes in Computer Science","Temporal Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0014000","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,20]],"date-time":"2021-07-20T07:31:46Z","timestamp":1626766306000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014000"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354058241X"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/bfb0014000","relation":{},"subject":[]}}