{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:17:42Z","timestamp":1725455862653},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540619840"},{"type":"electronic","value":"9783540495734"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0024435","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T01:41:39Z","timestamp":1132364499000},"page":"341-373","source":"Crossref","is-referenced-by-count":5,"title":["A case study in verification based on trace abstractions"],"prefix":"10.1007","author":[{"given":"Nils","family":"Klarlund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mogens","family":"Nielsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim","family":"Sunesen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"12_CR1","unstructured":"This volume."},{"issue":"2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"12_CR3","unstructured":"M. Abadi and L. Lamport. Conjoining specifications. Technical Report Report 118, Digital Equipment Corporation, Systems Research Center, 1993."},{"key":"12_CR4","unstructured":"M. Broy and L. Lamport. The RPC-Memory Specification Problem. A case study for the Dagstuhl Seminar 9439. This volume."},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"E.M. Clark, I.A. Browne, and R.P. Kurshan. A unified approach for showing language containment and equivalence between various types of \u03c9-automata. In A. Arnold, editor, CAAP, LNCS 431, pages 103\u2013116, 1990.","DOI":"10.1007\/3-540-52590-4_43"},{"issue":"1","key":"12_CR6","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: A semantics-based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 15(1):36\u201372, jan 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 16, pages 995\u20131072. MIT Press\/Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"U. Engberg, P. Gr\u00f8nning, and L. Lamport. Mechanical verification of concurrent systems with tla. In Computer Aided Verification, CAV '92. Springer-Verlag, 1993. Lecture Notes in Computer Science, Vol. 663.","DOI":"10.1007\/3-540-56496-9_5"},{"key":"12_CR9","unstructured":"U. Engberg. Reasoning in temporal logic of actions. Ph.D. Thesis, 1996."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Z. Har'El and R.P. Kurshan. Software for analytical development of communications protocols. Technical report, AT&T Technical Journal, 1990.","DOI":"10.1002\/j.1538-7305.1990.tb00102.x"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"J.G. Henriksen, O.J.L. Jensen, M.E. J\u00f8rgensen, N. Klarlund, R. Paige, T. Rauhe, and A.B. Sandholm. Mona: Monadic second-order logic in practice. In U.H. Engberg, K.G. Larsen, and A. Skou, editors, Procedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 58\u201373, 1995. BRICS Notes Series NS-95-2.","DOI":"10.7146\/brics.v2i21.19923"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science, Vol. 803","first-page":"273","volume-title":"A Decade of Concurrency","author":"Y. Kesten","year":"1993","unstructured":"Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification and simulation and refinement. In A Decade of Concurrency, pages 273\u2013346. ACM, Springer-Verlag, 1993. Lecture Notes in Computer Science, Vol. 803, Proceedings of the REX School\/Symposium, Noordwijkerhout, The Netherlands, June 1993."},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"N. Klarlund, M. Nielsen, and K. Sunesen. Automated logical verification based on trace abstractions. In Proc. Fifteenth ACM Symp. on Princ. of Distributed Computing (PODC). ACM, 1996.","DOI":"10.1145\/248052.248069"},{"issue":"1","key":"12_CR15","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.1993.1064","volume":"107","author":"N. Klarlund","year":"1993","unstructured":"N. Klarlund and F.B. Schneider. Proving nondeterministically specified safety properties using progress measures. Information and Computation, 107(1):151\u2013170, 1993.","journal-title":"Information and Computation"},{"key":"12_CR16","unstructured":"N. Klarlund and M.I. Schwartzbach. Logical programming for regular trees. In preparation, 1996."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"R. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton Univ. Press, 1994.","DOI":"10.1515\/9781400864041"},{"issue":"2","key":"12_CR18","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190\u2013222, 1983.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"12_CR19","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. Sixth Symp. on the Principles of Distributed Computing, pages 137\u2013151. ACM, 1987.","DOI":"10.1145\/41840.41852"},{"key":"12_CR21","unstructured":"N. Lynch and F. W. Vaandrager. Forward and backward simulations \u2014 part I: untimed systems. Technical Report CS-R9313, Centrum voor Wiskunde en Informatica, CWI, Computer Science\/Department of Software Technology, 1993."},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Z. Manna and et al. STeP: The stanford temporal prover. In Theory and Practice of Software Development (TAPSOFT). Springer-Verlag, 1995. Lecture Notes in Computer Science, Vol. 915.","DOI":"10.1007\/3-540-59293-8_237"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. PhD thesis, Carnegie Mellon University, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"1","key":"12_CR25","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0020-0190(89)90063-X","volume":"32","author":"A.P. Sistla","year":"1989","unstructured":"A.P. Sistla. On verifying that a concurrent program satisfies a nondeterministic specification. Information Processing Letters, 32(1):17\u201324, July 1989.","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Formal Systems Specification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0024435","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T10:01:00Z","timestamp":1683280860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0024435"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619840","9783540495734"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0024435","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}