{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:18Z","timestamp":1776305058076,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540665595","type":"print"},{"value":"9783540481539","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_6","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:13:28Z","timestamp":1269882808000},"page":"54-66","source":"Crossref","is-referenced-by-count":154,"title":["Model Checking TLA+ Specifications"],"prefix":"10.1007","author":[{"given":"Yuan","family":"Yu","sequence":"first","affiliation":[]},{"given":"Panagiotis","family":"Manolios","sequence":"additional","affiliation":[]},{"given":"Leslie","family":"Lamport","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"6_CR1","unstructured":"Alpha Architecture Committee. Alpha Architecture Reference Manual. Digital Press, Boston, third edition, 1998."},{"key":"6_CR2","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/S0022-0000(75)80018-3","volume":"10","author":"E. A. Ashcroft","year":"1975","unstructured":"E. A. Ashcroft. Proving assertions about parallel programs. Journal of Computer and System Sciences, 10:110\u2013135, February 1975.","journal-title":"Journal of Computer and System Sciences"},{"key":"6_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logics of Programs, volume 131 of LNCS. Springer-Verlag, 1981."},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic. ACM Transactions on Programming Languages and Systems, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"David L. Dill. The Mur\u03d5 verification system. In Computer Aided Verification. 8th International Conference, pages 390\u2013393, 1996.","DOI":"10.1007\/3-540-61474-5_86"},{"issue":"1","key":"6_CR6","first-page":"44","volume":"69","author":"Z. Har\u2019El","year":"1990","unstructured":"Z. Har\u2019El and R. P. Kurshan. Software for analytical development of communication protocols. AT&T Technical Journal, 69(1):44\u201359, 1990.","journal-title":"AT&T Technical Journal"},{"key":"6_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-56922-7_14","volume-title":"Computer-Aided Verification","author":"Kurshan","year":"1993","unstructured":"Kurshan and Leslie Lamport. Verification of a multiplier: 64 bits and beyond. In Costas Courcoubetis, editor, Computer-Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 166\u2013179, Berlin, June 1993. Springer-Verlag. Proceedings of the Fifth International Conference, CAV\u201993."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Peter Ladkin, Leslie Lamport, Bryan Olivier, and Denis Roegel. Lazy caching in TLA. Distributed Computing, 12, 1999. To appear.","DOI":"10.1007\/s004460050063"},{"key":"6_CR9","unstructured":"Leslie Lamport. TLA-temporal logic of actions. At URL http:\/\/www.research.digital.com\/SRC\/tla\/ on the World Wide Web. It can also be found by searching the Web for the 21-letter string formed by concatenating uid and lamporttlahomepage."},{"issue":"9","key":"6_CR10","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"C-28","author":"L. Lamport","year":"1979","unstructured":"Leslie Lamport. How to make a multiprocessorcomputer that correctly executes multiprocess programs. IEEE Transactions on computer, C-28(9):690\u2013691, September 1979.","journal-title":"IEEE Transactions on computer"},{"key":"6_CR11","volume-title":"Introduction to TLA","author":"L. Lamport","year":"1994","unstructured":"Leslie Lamport. Introduction to TLA. Technical Report 1994-001, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, December 1994."},{"issue":"3","key":"6_CR12","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamprt","year":"1994","unstructured":"Leslie Lamprt. The temporal logic of actions. ACM Transactions on Programming Languages and System, 16(3):872\u2013923, May 1994.","journal-title":"ACM Transactions on Programming Languages and System"},{"key":"6_CR13","first-page":"183","volume-title":"Calculational System Design","author":"L. Lamport","year":"1999","unstructured":"Leslie Lamport. Specifying concurrent systems with tla+. In Manfred. Broy and Ralf Steinbr\u00fcggen, editors, Calculational System Design, pages 183\u2013247, Amsterdam, 1999. IOS Press."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"5","key":"6_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S. Owicki","year":"1976","unstructured":"Susan Owicki and David Gries. Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM, 19(5):279\u2013284, May 1976.","journal-title":"Communications of the ACM"},{"key":"6_CR16","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Proc. of the 5th International Symposium on Programming","author":"J. P. Queille","year":"1981","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. of the 5th International Symposium on Programming, volume 137 of LNCS, pages 337\u2013350, 1981."},{"key":"6_CR17","series-title":"Technical Report TR-15-81","volume-title":"Fingerprinting by random polynomials","author":"M. O. Rabin","year":"1981","unstructured":"M. O. Rabin. Fingerprinting by random polynomials. Technical Report TR-15-81, Center for Research in Computing Technology, Harvard University, 1981."},{"key":"6_CR18","unstructured":"A. W. R oscoe. Model-checking CSP. In A Classical Mind: Essays in Honour of C A R Hoare, International Series in Computer Science, chapter 21, pages 353\u2013378. Prentice-Hall International, 1994."},{"key":"6_CR19","unstructured":"Ulrich Stern. Algorithmic Techniques in Verification by Explicit State Enumeration. PhD thesis, Technical University of Munich, 1997."},{"key":"6_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0028743","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1998","unstructured":"Ulrich Stern and David L. Dill. Using magnetic disk instead of main memory in the Mur\u03d5 verifier. In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 172\u2013183, Berlin, June 1998. Springer-Verlag. 10th International Conference, CAV\u201998."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T15:01:52Z","timestamp":1558969312000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}