{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T06:40:26Z","timestamp":1737355226707,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672821"},{"type":"electronic","value":"9783540464198"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_10","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T23:17:25Z","timestamp":1186615045000},"page":"127-141","source":"Crossref","is-referenced-by-count":1,"title":["On Memory-Block Traversal Problems in Model-Checking Timed Systems"],"prefix":"10.1007","author":[{"given":"Fredrik","family":"Larsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wang","family":"Yi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"10_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Proc. of Int. Colloquium on Algorithms, Languages and Programming","author":"R. Alur","year":"1990","unstructured":"Rajeev Alur and David Dill. Automata for Modelling Real-Time Systems. In Proc. of Int. Colloquium on Algorithms, Languages and Programming, number 443 in Lecture Notes in Computer Science, pages 322\u2013335, July 1990. 129"},{"key":"10_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031985","volume-title":"Proc. of REX Workshop \u201cReal-Time: Theory in Practice\u201d","author":"M. Abadi","year":"1992","unstructured":"Martin Abadi and Leslie Lamport. An Old-Fashioned Recipe for Real Time. In Proc. of REX Workshop \u201cReal-Time: Theory in Practice\u201d, number 600 in Lecture Notes in Computer Science, 1992. 137"},{"key":"10_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-61474-5_73","volume-title":"Proc. of the 8th Int. Conf. on Computer Aided Verification","author":"BGK+96. Bengtsson","year":"1996","unstructured":"BGK+96._Johan Bengtsson, W.O. David Griffioen, K\u00e4re J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Verification of an Audio Protocol with Bus Collision Using Uppaal. In Rajeev Alur and Thomas A. Henzinger, editors, Proc. of the 8th Int. Conf. on Computer Aided Verification, number 1102 in Lecture Notes in Computer Science, pages 244\u2013256. Springer-Verlag, July 1996. 127"},{"key":"10_CR4","unstructured":"BLL+98._Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi, and Carsten Weise. New Generation of Uppaal. In Int. Workshop on Software Tools for Technology Transfer, June 1998. 127"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Hans-J. Boehm. Space Efficient Conservative Garbage Collection. In Proc. of the ACM SIGPLAN\u2019 91 Conference on Programming Language Design and Implementation, pages 197\u2013206, 1993. 140","DOI":"10.1145\/173262.155109"},{"key":"10_CR6","series-title":"Lect Notes Comput Sci","first-page":"208","volume-title":"Proc. of Workshop on Verification and Control of Hybrid Systems III","author":"C. Daws","year":"1995","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool kronos. In Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag, editors, Proc. of Workshop on Verification and Control of Hybrid Systems III, number 1066 in Lecture Notes in Computer Science, pages 208\u2013219. Springer-Verlag, October 1995. 127"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Thomas A. Henzinger and Pei-Hsin Ho. HyTech: The Cornell HYbrid TECHnology Tool. In Proc. of TACAS, Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 1995. BRICS report series NS-95-2. 127","DOI":"10.1007\/3-540-60472-3_14"},{"issue":"2","key":"10_CR8","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"Thomas. A. Henzinger","year":"1994","unstructured":"Thomas. A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic Model Checking for Real-Time Systems. Information and Computation, 111(2):193\u2013244, 1994. 130","journal-title":"Information and Computation"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Klaus Havelund, Arne Skou, Kim G. Larsen, and Kristian Lund. Formal Modeling and Analysis of an Audio\/Video Protocol: An Industrial Case Study Using Uppaal. In Proc. of the 18th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, December 1997. 137","DOI":"10.7146\/brics.v4i31.18957"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"KLL+97._K\u00e5re J. Kristoffersen, Francois Laroussinie, Kim G. Larsen, Paul Pettersson, and Wang Yi. A Compositional Proof of a Real-Time Mutual Exclusion Protocol. In Proc. of the 7th Int. Joint Conf. on the Theory and Practice of Software Development, April 1997. 137","DOI":"10.1007\/BFb0030626"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Henrik L\u00f6nn and Paul Pettersson. Formal Verification of a TDMA Protocol Startup Mechanism. In Proc. of the Pacific Rim Int. Symp. on Fault-Tolerant Systems, pages 235\u2013242, December 1997. 128, 137","DOI":"10.1109\/PRFTS.1997.640153"},{"issue":"1\u20132","key":"10_CR12","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1\u20132):134\u2013152, October 1997. 127","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"10_CR13","unstructured":"Paul Pettersson. Modelling and Analysis of Real-Time Systems Using Timed Automata: Theory and Practice. PhD thesis, Department of Computer Systems, Uppsala University, February 1999. 130, 131"},{"key":"10_CR14","unstructured":"Tomas Gerhard Rokicki. Representing and Modeling Digital Circuits. PhD thesis, Stanford University, 1993. 130"},{"key":"10_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 10th Int. Conf. on Computer Aided Verification","author":"U. Stern","year":"1998","unstructured":"Ulrich Stern and David L. Dill. Using Magnetic Disk instead of Main Memory in the Murphi Verifier. In Proc. of the 10th Int. Conf. on Computer Aided Verification, Lecture Notes in Computer Science. Springer-Verlag, June 1998. 140"},{"key":"10_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the International Workshop on Memory Management","author":"P. R. Wilson","year":"1992","unstructured":"Paul R. Wilson. Uniprocessor Garbage Collection Techniques. In Proc. of the International Workshop on Memory Management, number 637 in LNCS. Springer-Verlag, 1992. 140"},{"key":"10_CR17","unstructured":"Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In Dieter Hogrefe and Stefan Leue, editors, Proc. of the 7th Int. Conf. on Formal Description Techniques, pages 223\u2013238. North-Holland, 1994. 130"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T06:00:22Z","timestamp":1737352822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}