{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:23Z","timestamp":1725490223731},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665878"},{"type":"electronic","value":"9783540481195"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48119-2_13","type":"book-chapter","created":{"date-parts":[[2007,8,28]],"date-time":"2007-08-28T21:23:00Z","timestamp":1188336180000},"page":"195-211","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Error Detection with Directed Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Frank","family":"Reffe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Edelkamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"13_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/3-540-63166-6_34","volume-title":"Computer Aided Verication","author":"R. Alur","year":"1997","unstructured":"R. Alur, R. Brayton, T. Henzinger, S. Qaderer, and S. Rajamani. Partial-order reduction in symbolic state space exploration. In Computer Aided Verication, volume 1254 of LNCS, pages 340\u2013351, 1997."},{"key":"13_CR2","unstructured":"A. Biere. Effiziente \u00b5-Kalk\u00f6l Modellpr\u00f6fung mit Bin\u00e4aren Entscheidungsdiagrammen.PhD thesis, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, 1997."},{"key":"13_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"468","DOI":"10.1007\/3-540-63166-6_50","volume-title":"Computer Aided Verication","author":"A. Biere","year":"1997","unstructured":"A. Biere. mucke-efficient \u00b5-calculus model checking. InComputer Aided Verication, volume 1254 of LNCS, pages 468\u2013471, 1997."},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems, 1999. to appear.","DOI":"10.21236\/ADA360973"},{"issue":"8","key":"13_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant. Graph based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"13_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0028174","volume-title":"Decade of Concurrency","author":"E. Clarke","year":"1993","unstructured":"E. Clarke, O. Grumberg, and D. Long. Verification tools for finite-state concurrent systems. In A Decade of Concurrency, volume 803 of LNCS, pages 124\u2013175. REX School Symposium, Springer, 1993."},{"key":"13_CR7","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"R. Cleaveland. Tableau-based model checking in the propositional \u00b5-calculus. Acta Inf., 27:725\u2013747, 1990.","journal-title":"Acta Inf."},{"issue":"5","key":"13_CR8","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. Numerical Mathematics, 1(5):269\u2013271, 1959.","journal-title":"Numerical Mathematics"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits.An ACM Distinguished Dissertation. The MIT Press, 1988.","DOI":"10.7551\/mitpress\/6874.001.0001"},{"issue":"1","key":"13_CR10","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/0004-3702(94)90040-X","volume":"65","author":"J. F. Dillenburg","year":"1994","unstructured":"J. F. Dillenburg and P. C. Nelson. Perimeter search (research note). Articial Intelligence,65(1):165\u2013178, Jan. 1994.","journal-title":"Articial Intelligence"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"S. Edelkamp and F. Reffel.OBDDs in heuristic search. In O. Herzog and A. G\u00fcnter, editors, Proceedings of the 22nd Annual German Conference on Advances in Articial Intelligence (KI-98), volume 1504 of LNAI, pages 81\u201392. Springer, 1998.","DOI":"10.1007\/BFb0095430"},{"key":"13_CR12","series-title":"Technical Report","volume-title":"Deterministic state space planning with BDDs","author":"S. Edelkamp","year":"1999","unstructured":"S. Edelkamp and F. Reffel. Deterministic state space planning with BDDs. Technical Report 120, Institut f\u00fcr Informatik, Universit\u00e4 Freiburg, 1999."},{"key":"13_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BFb0013022","volume-title":"REX workshop","author":"E. A. Emerson","year":"1989","unstructured":"E. A. Emerson and J. Srinivasan. Branching time temporal logic. In REX workshop, volume 354 of LNCS, pages 123\u2013172. Springer-Verlag, 1989."},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BF00121127","volume":"1","author":"J. C. Fernandez","year":"1992","unstructured":"J. C. Fernandez, L. Mounier, C. Jard, and T. J\u00e9ron. On-the-fly verification of finite transition systems. Formal Methods in System Design, 1:251\u2013273, 1992.","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"13_CR15","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","volume":"SCC-4","author":"P. Hart","year":"1968","unstructured":"P. Hart, N. Nilsson, and B. Raphael. A formal basis for the heuristic determination of minimum cost paths. IEEE Transactions of Systems Science and Cybernetics, SCC-4(2):100\u2013107, 1968.","journal-title":"IEEE Transactions of Systems Science and Cybernetics"},{"key":"13_CR16","first-page":"97","volume-title":"Articial Intelligence","author":"R. E. Korf","year":"1985","unstructured":"R. E. Korf. Depth-rst iterative-deepening: An optimal admissible tree search. Articial Intelligence, 27(1):97\u2013109, 1985. reprinted in Chapter 6 of Expert Systems, A Software Methodology for Modern Applications, P.G. Raeth (Ed.), IEEE Computer Society Press, Washington D.C., 1990, pp. 380\u2013389."},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that nite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 97\u2013107, New York, 1985. ACM.","DOI":"10.1145\/318593.318622"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Press, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"13_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Concurrency and automata on infinite sequences","author":"D. Park","year":"1981","unstructured":"D. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Theoretical Computer Science, 5th GI Conference, volume 104 of LNCS, pages 167\u2013183.Springer, 1981."},{"key":"13_CR21","unstructured":"J. Pearl. Heuristics: Intelligent search strategies for computer problem solving. Addison-Wesley series in Articial Intelligence. Addison-Wesley, 1984."},{"issue":"7","key":"13_CR22","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1109\/34.297950","volume":"16","author":"A. Reinefeld","year":"1994","unstructured":"A. Reinefeld and T. A. Marsland. Enhanced iterative-deepening search. IEEE Transactions on Pattern Analysis and Machine Intelligence, 16(7):701\u2013710, 1994.","journal-title":"IEEE Transactions on Pattern Analysis and Machine Intelligence"},{"key":"13_CR23","unstructured":"R. Rudell. Dynamic variable ordering for ordered binary decision diagrams.In International Conference on Computer-Aided Design, pages 139\u2013144. IEEE, 1993."},{"key":"13_CR24","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C. Stirling","year":"1991","unstructured":"C. Stirling and D. Walker. Local model checking in the modal \u00b5-calculus. Theoretical Computer Science, 89:161\u2013177, 1991.","journal-title":"Theoretical Computer Science"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"C. H. Yang and D. Dill. Validation with guided search of the state space. In 35nd Design Automation Conference, 1998.","DOI":"10.1145\/277044.277201"}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48119-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T21:29:31Z","timestamp":1558474171000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48119-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665878","9783540481195"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-48119-2_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"17 September 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}