{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T09:39:02Z","timestamp":1791106742824,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540421245","type":"print"},{"value":"9783540451396","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45139-0_5","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:39:56Z","timestamp":1186742396000},"page":"57-79","source":"Crossref","is-referenced-by-count":95,"title":["Directed explicit model checking with HSF-SPIN"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Edelkamp","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alberto Lluch","family":"Lafuente","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Leue","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,5,2]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"A. Biere. \u03bccke-efficient \u03bc-calculus model checking. In Computer Aided Verification, pages 468\u2013471, 1997.","DOI":"10.1007\/3-540-63166-6_50"},{"issue":"2","key":"5_CR2","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323\u2013342, Apr 1983.","journal-title":"Journal of the ACM"},{"key":"5_CR3","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000."},{"key":"5_CR4","unstructured":"T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, 1990."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"A. D. E. Muller and P. Schnupp. Alternating automata. the weak monadic theory of the tree and its complexity. In International Colloquim on Automata, Languages and Programming.","DOI":"10.1007\/3-540-16761-7_77"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"R. Dial. Shortest path forest with topological ordering. Communications of the ACM, pages 632\u2013633, 1969.","DOI":"10.1145\/363269.363610"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BF01386390","volume":"1","author":"E. W. Dijkstra","year":"1959","unstructured":"E. W. Dijkstra. A note on two problems in connection with graphs. Numerische Mathematik, 1:269\u2013271, 1959.","journal-title":"Numerische Mathematik"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Patterns in property specifications for finite-state verification. In International Conference on Software Engineering, 1999.","DOI":"10.1145\/302405.302672"},{"key":"5_CR9","unstructured":"S. Edelkamp. Data Structures and Learning Algorithms in State Space Search. PhD thesis, University of Freiburg, 1999. Infix."},{"key":"5_CR10","unstructured":"S. Edelkamp, A. L. Lafuente, and S. Leue. Protocol verification with heuristic search. In AAAI Symposium on Model-based Validation of Intelligence, 2001."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"S. Edelkamp and F. Reffel. OBDDs in heuristic search. In German Conference on Artificial Intelligence (KI), pages 81\u201392, 1998.","DOI":"10.1007\/BFb0095430"},{"issue":"9","key":"5_CR12","doi-asserted-by":"publisher","first-page":"969","DOI":"10.1016\/0169-7552(93)90094-K","volume":"25","author":"M. G. Gouda","year":"1993","unstructured":"M. G. Gouda. Protocol verification made simple: a tutorial. Computer Networks and ISDN Systems, 25(9):969\u2013980, 1993.","journal-title":"Computer Networks and ISDN Systems"},{"key":"5_CR13","first-page":"100","volume":"4","author":"P. E. Hart","year":"1968","unstructured":"P. E. Hart, N. J. Nilsson, and B. Raphael. A formal basis for heuristic determination of minimum path cost. IEEE Trans. on SSC, 4:100, 1968.","journal-title":"IEEE Trans. on SSC"},{"issue":"3","key":"5_CR14","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1023\/A:1008696026254","volume":"13","author":"G. Holzmann","year":"1998","unstructured":"G. Holzmann. An analysis of bitstate hashing. Formal Methods in System Design, 13(3):287\u2013305, November 1998. extended and revised version of Proc. PSTV95, pp. 301-314.","journal-title":"Formal Methods in System Design"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"G. Holzmann, D. Peled, and M. Yannakakis. On nested depth first search. In The Spin Verification System, pages 23\u201332. American Mathematical Society, 1996.","DOI":"10.1090\/dimacs\/032\/03"},{"key":"5_CR16","unstructured":"G. J. Holzmann. On limits and possibilities of automated protocol analysis. In Protocol Specification, Testing, and Verification, 1987."},{"key":"5_CR17","unstructured":"G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1990."},{"key":"5_CR18","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/s100090050045","volume":"2","author":"M. Kamel","year":"2000","unstructured":"M. Kamel and S. Leue. Formalization and validation of the general inter-orb protocol (GIOP) using Promela and SPIN. In Software Tools for Technology Transfer, volume 2, pages 394\u2013409, 2000.","journal-title":"Software Tools for Technology Transfer"},{"key":"5_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1007\/3-540-46419-0_32","volume-title":"6th International Conference, TACAS 2000","author":"M. Kamel","year":"2000","unstructured":"M. Kamel and S. Leue. Vip: A visual editor and compiler for v-promela. In 6th International Conference, TACAS 2000, volume 1785 of Lecture Notes in Computer Science, pages 471\u2013486. Springer, 2000."},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"F. J. Lin, P. M. Chu, and M. Liu. Protocol verification using reachability analysis: the state space explosion problem and relief strategies. ACM, pages 126\u2013135, 1988.","DOI":"10.1145\/55483.55496"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Press, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"D. McVitie and L. Wilson. The stable marriage problem. Communications of the ACM, 1971.","DOI":"10.1145\/362619.362631"},{"key":"5_CR23","unstructured":"A. Miller and M. Calder. Analysing a basic call protocol using promela\/xspin. In International SPIN Workshop, 1998."},{"key":"5_CR24","unstructured":"T. Nakatani. Verification of group address registration protocol using promela and spin. In International SPIN Workshop, 1997."},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"K. R. Bloem and F. Somenzi. Symbolic guided search for ctl model checking. In Conference on Design Automation (DAC-00).","DOI":"10.1145\/337292.337306"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"F. Reffel and S. Edelkamp. Error detection with directed symbolic model checking. In World Congress on Formal Methods, pages 195\u2013211. Springer, 1999.","DOI":"10.1007\/3-540-48119-2_13"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"F. Somenzi and R. Bloem. Efficient buchi automata from ltl formulae. In Computer Aided Verification.","DOI":"10.1007\/10722167_21"},{"key":"5_CR28","unstructured":"P. van Eijk. Verifying relay circuits using state machines. In International SPIN Workshop."},{"key":"5_CR29","unstructured":"W. Visser and H. Barringer. Ctl* model checking for spin. Software Tools for Technology Transfer, 2000."},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"C. H. Yang and D. L. Dill. Validation with guided search of the state space. In DAC, pages 599\u2013604, 1998.","DOI":"10.1145\/277044.277201"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45139-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:17:39Z","timestamp":1556734659000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45139-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421245","9783540451396"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-45139-0_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}