{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:54:33Z","timestamp":1725544473152},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540331025"},{"type":"electronic","value":"9783540331032"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11691617_2","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T14:14:13Z","timestamp":1143555253000},"page":"19-34","source":"Crossref","is-referenced-by-count":12,"title":["Directed Model Checking with Distance-Preserving Abstractions"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Dr\u00e4ger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-45319-9_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.: Efficient guiding towards cost-optimality in uppaal. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 174\u2013188. Springer, Heidelberg (2001)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking. In: Design Automation Conference, pp. 29\u201334 (2000)","DOI":"10.1145\/337292.337306"},{"issue":"2","key":"2_CR3","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/s00165-004-0034-9","volume":"16","author":"H. Dierks","year":"2004","unstructured":"Dierks, H.: Comparing model checking and logical reasoning for real-time systems. Formal Aspects of Computing\u00a016(2), 104\u2013120 (2004)","journal-title":"Formal Aspects of Computing"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Software Tools for Technology Transfer (2003)","DOI":"10.1007\/s10009-002-0104-3"},{"key":"2_CR5","unstructured":"Edelkamp, S., Lluch-Lafuente, A.: Abstraction databases in theory and model checking. In: Proc. ICAPS Workshop on Connecting Planning Theory with Practice (June 2004)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45139-0_5","volume-title":"Model Checking Software","author":"S. Edelkamp","year":"2001","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 57\u201379. Springer, Heidelberg (2001)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Trail-directed model checking. Electr. Notes Theor. Comput. Sci.\u00a055(3) (2001)","DOI":"10.1016\/S1571-0661(04)00261-0"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S. Graf","year":"1996","unstructured":"Graf, S., Steffen, B., L\u00fcttgen, G.: Compositional minimization of finite state systems using interface specifications. Formal Aspects of Computing\u00a08, 607\u2013616 (1996)","journal-title":"Formal Aspects of Computing"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-46017-9_21","volume-title":"Model Checking Software","author":"A. Groce","year":"2002","unstructured":"Groce, A., Visser, W.: Heuristics for model checking Java programs. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 242\u2013245. Springer, Heidelberg (2002)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-540-40007-3_25","volume-title":"Formal Methods at the Crossroads. From Panacea to Foundational Support","author":"M. Kaltenbach","year":"2003","unstructured":"Kaltenbach, M., Misra, J.: A theory of hints in model checking. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol.\u00a02757, pp. 423\u2013438. Springer, Heidelberg (2003)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1186","DOI":"10.1007\/3-540-48118-4_13","volume-title":"FM\u201999 - Formal Methods","author":"B. Krieg-Br\u00fcckner","year":"1999","unstructured":"Krieg-Br\u00fcckner, B., Peleska, J., Olderog, E.-R., Baer, A.: The UniForM workbench, a universal development environment for formal methods. In: Wing, J., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01709, p. 1186. Springer, Heidelberg (1999)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/11691617_3","volume-title":"Model Checking Software","author":"S. Kupferschmid","year":"2006","unstructured":"Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 35\u201352. Springer, Heidelberg (2006)"},{"key":"2_CR13","unstructured":"Lafuente, A.L.: Directed Search for the Verification of Communication Protocols. PhD thesis, Institute of Computer Science, University of Freiburg (June 2003)"},{"issue":"1, 2","key":"2_CR14","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. Larsen","year":"1997","unstructured":"Larsen, K., Petterson, P., Yi, W.: Uppaal in a nutshell. STTT \u2013 International Journal on Software Tools for Technology Transfer\u00a01(1, 2), 134\u2013152 (1997)","journal-title":"STTT \u2013 International Journal on Software Tools for Technology Transfer"},{"issue":"1","key":"2_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/272991.272995","volume":"8","author":"M. Matsumoto","year":"1998","unstructured":"Matsumoto, M., Nishimura, T.: Mersenne Twister: A 623-dimensionally equidistributed uniform pseudo-random number generator. ACM Transactions on Modeling and Computer Simulation\u00a08(1), 3\u201330 (1998)","journal-title":"ACM Transactions on Modeling and Computer Simulation"},{"key":"2_CR16","volume-title":"Heuristics","author":"J. Pearl","year":"1983","unstructured":"Pearl, J.: Heuristics. Morgan Kaufmann, San Francisco (1983)"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-540-24730-2_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Qian","year":"2004","unstructured":"Qian, K., Nymeyer, A.: Guided invariant model checking based on abstraction and symbolic pattern databases. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 497\u2013511. Springer, Heidelberg (2004)"},{"issue":"9","key":"2_CR18","doi-asserted-by":"publisher","first-page":"940","DOI":"10.1109\/26.35374","volume":"37","author":"K.K. Sabnani","year":"1989","unstructured":"Sabnani, K.K., Lapone, A.M., Uyar, M.\u00dc.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun.\u00a037(9), 940\u2013948 (1989)","journal-title":"IEEE Trans. Commun."},{"key":"2_CR19","unstructured":"Seitz, C.: Ideas about arbiters. Lambda, 10\u201314 (1980)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Design Automation Conference, pp. 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\/11691617_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,17]],"date-time":"2019-04-17T17:18:47Z","timestamp":1555521527000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691617_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540331025","9783540331032"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11691617_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}