{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T09:58:46Z","timestamp":1781258326051,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540417910","type":"print"},{"value":"9783540452515","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45251-6_6","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T01:53:28Z","timestamp":1186883608000},"page":"99-118","source":"Crossref","is-referenced-by-count":23,"title":["How to Make FDR Spin LTL Model Checking of CSP by Refinement"],"prefix":"10.1007","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew","family":"Currie","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thierry","family":"Massart","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,3,16]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B-Book. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"issue":"4","key":"6_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21(4):181\u2013185, October 1985.","journal-title":"Information Processing Letters"},{"key":"6_CR3","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli. The temporal logic of concurrent programs. Theoretical Computer Science, 13:45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"6_CR4","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. Bryant","year":"1992","unstructured":"R. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293\u2013318, September 1992.","journal-title":"ACM Computing Surveys"},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/BF01214622","volume":"7","author":"M. Butler","year":"1995","unstructured":"M. Butler and C. Morgan. Action systems, unbounded nondeterminism, and infinite traces. Formal Aspects of Computing, 7:37\u201353, 1995.","journal-title":"Formal Aspects of Computing"},{"key":"6_CR6","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"issue":"2","key":"6_CR7","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"6_CR8","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E. M. Clarke","year":"1996","unstructured":"E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626\u2013643, Dec. 1996.","journal-title":"ACM Computing Surveys"},{"key":"6_CR9","unstructured":"S. J. Creese and A. W. Roscoe. Data independent induction over structured networks. In International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA\u2019 00), Las Vegas, USA, June 2000."},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"M. Leuschel, T. Massart, and A. Currie. How to make FDR spin: LTL model checking of CSP by refinement. Technical Report DSSE-TR-2000-10, Department of Electronics and Computer Science, University of Southampton, September 2000.","DOI":"10.1007\/3-540-45251-6_6"},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002360050074","volume":"34","author":"J. Esparza","year":"1997","unstructured":"J. Esparza. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85\u2013107, 1997.","journal-title":"Acta Informatica"},{"key":"6_CR12","unstructured":"Formal Systems (Europe) Ltd. Failures-Divergence Refinement \u2014 FDR2 User Manual."},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. 15th Workshop on Protocol Specification, Testing, and Verification, Warsaw, June 1995. North-Holland.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"C. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"6_CR15","unstructured":"G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"key":"6_CR16","series-title":"Lect Notes Comput Sci","first-page":"63","volume-title":"Proceedings of LOPSTR\u201999","author":"M. Leuschel","year":"1999","unstructured":"M. Leuschel and T. Massart. In_nite state model checking by abstract interpretation and program specialisation. In A. Bossi, editor, Proceedings of LOPSTR\u201999, LNCS 1817, pages 63\u201382, Venice, Italy, September 1999."},{"key":"6_CR17","unstructured":"J. Magee and J. Kramer. Concurrency: State Models & Java Programs. Wiley, 1999."},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. PhD thesis, Boston, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"6_CR19","unstructured":"A. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1997."},{"key":"6_CR20","unstructured":"A. W. Roscoe and R. S. Lazic. Using logical relations for automated verification of data-independent CSP. In Proceedings of Oxford Workshop on Automated Formal Methods ENTCS, 1996."},{"key":"6_CR21","unstructured":"R. Sedgewick. Algorithms in C++. Addison-Wesley, 1992."},{"issue":"3","key":"6_CR22","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1985","unstructured":"A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733\u2013749, July 1985.","journal-title":"Journal of the ACM"},{"key":"6_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/3-540-56922-7_33","volume-title":"Proceedings of CAV\u201993","author":"A. Valmari","year":"1993","unstructured":"A. Valmari. On-the-fly veri_cation with stubborn sets. In C. Courcoubetis, editor, Proceedings of CAV\u201993, LNCS 697, pages 397\u2013408. Springer-Verlag, 1993."},{"key":"6_CR24","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of LICS\u201986, pages 332\u2013344, 1986."}],"container-title":["Lecture Notes in Computer Science","FME 2001: Formal Methods for Increasing Software Productivity"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45251-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:49:04Z","timestamp":1556740144000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45251-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417910","9783540452515"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45251-6_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}