{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T00:21:41Z","timestamp":1743034901672,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":54,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642206733"},{"type":"electronic","value":"9783642206740"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-20674-0_3","type":"book-chapter","created":{"date-parts":[[2011,4,20]],"date-time":"2011-04-20T06:06:05Z","timestamp":1303279565000},"page":"32-51","source":"Crossref","is-referenced-by-count":1,"title":["Program Model Checking via Action Planning"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Edelkamp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Kellershoff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Damian","family":"Sulewski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Albarghouthi, A., Baier, J., McIlraith, S.A.: On the use of planning technology for verification. In: Workshop on ICAPS 2009 (2009)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-28644-8_1","volume-title":"CONCUR 2004 - Concurrency Theory","author":"T. Andrews","year":"2004","unstructured":"Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: Exploiting program structure for model checking concurrent software. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 1\u201315. Springer, Heidelberg (2004)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-00431-5_2","volume-title":"Model Checking and Artificial Intelligence","author":"M. Bakera","year":"2009","unstructured":"Bakera, M., Edelkamp, S., Kissmann, P., Renner, C.D.: Solving \u03bc-calculus parity games by symbolic planning. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS, vol.\u00a05348, pp. 15\u201333. Springer, Heidelberg (2009)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"3_CR5","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-540-89287-8_11","volume":"1","author":"B. Bonet","year":"2008","unstructured":"Bonet, B., Haslum, P., Hickmott, S.L., Thi\u00e9baux, S.: Directed unfolding of Petri nets. T. Petri Nets and Other Models of Concurrency\u00a01, 172\u2013198 (2008)","journal-title":"T. Petri Nets and Other Models of Concurrency"},{"issue":"3","key":"3_CR6","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys\u00a024(3), 142\u2013170 (1992)","journal-title":"ACM Computing Surveys"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Bylander, T.: The computational complexity of propositional STRIPS planning. Artificial Intelligence, 165\u2013204 (1994)","DOI":"10.1016\/0004-3702(94)90081-7"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/3-540-63912-8_81","volume-title":"Recent Advances in AI Planning","author":"A. Cimatti","year":"1997","unstructured":"Cimatti, A., Giunchiglia, E., Giunchiglia, F., Traverso, P.: Planning via model checking: A decision procedure for AR. In: Steel, S. (ed.) ECP 1997. LNCS, vol.\u00a01348, pp. 130\u2013142. Springer, Heidelberg (1997)"},{"issue":"1-2","key":"3_CR9","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0004-3702(02)00374-0","volume":"147","author":"A. Cimatti","year":"2003","unstructured":"Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, strong, and strong cyclic planning via symbolic model checking. Artif. Intell.\u00a0147(1-2), 35\u201384 (2003)","journal-title":"Artif. Intell."},{"issue":"1-2","key":"3_CR10","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/j.artint.2004.05.003","volume":"159","author":"A. Cimatti","year":"2004","unstructured":"Cimatti, A., Roveri, M., Bertoli, P.: Conformant planning via symbolic model checking and heuristic search. Artif. Intell.\u00a0159(1-2), 127\u2013206 (2004)","journal-title":"Artif. Intell."},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kr\u00f6ning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kr\u00f6ning, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"issue":"5","key":"3_CR13","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"3_CR14","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B.: Bounded model checking of multi-threaded software using smt solvers, vol. abs\/1003.3830 (2010)","DOI":"10.1145\/1810295.1810396"},{"issue":"4","key":"3_CR16","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1111\/0824-7935.00065","volume":"14","author":"J.C. Culberson","year":"1998","unstructured":"Culberson, J.C., Schaeffer, J.: Pattern databases. Computational Intelligence\u00a014(4), 318\u2013334 (1998)","journal-title":"Computational Intelligence"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/11804192_7","volume-title":"Formal Methods for Components and Objects","author":"D. Dams","year":"2006","unstructured":"Dams, D., Namjoshi, K.S.: Orion: High-precision methods for static error analysis of C and C++ programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 138\u2013160. Springer, Heidelberg (2006)"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-642-00768-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N.H.M. Aan de Brugh","year":"2009","unstructured":"Aan de Brugh, N.H.M., Nguyen, V.Y., Ruys, T.C.: moonWalker: Verification of.NET programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 170\u2013173. Springer, Heidelberg (2009)"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-44829-2_13","volume-title":"Model Checking Software","author":"S. Edelkamp","year":"2003","unstructured":"Edelkamp, S.: Promela planning. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 197\u2013212. Springer, Heidelberg (2003)"},{"issue":"2","key":"3_CR20","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2005.07.023","volume":"149","author":"S. Edelkamp","year":"2006","unstructured":"Edelkamp, S., Jabbar, S.: Action planning for directed model checking of Petri nets. Electronic Notes in Theoretical Computer Science (ENTCS)\u00a0149(2), 3\u201318 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science (ENTCS)"},{"key":"3_CR21","unstructured":"Edelkamp, S., Jabbar, S., Lluch-Lafuente, A.: Action planning for graph transition systems. In: ICAPS 2005-Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (2005)"},{"issue":"2","key":"3_CR22","first-page":"44","volume":"22","author":"S. Edelkamp","year":"2008","unstructured":"Edelkamp, S., Jabbar, S., Midzic, D., Rikowski, D., Sulewski, D.: External memory search for verification of multi-threaded C++ programs. KI\u00a022(2), 44\u201350 (2008)","journal-title":"KI"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Jabbar, S., Sulewski, D.: Distributed verification of multi-threaded C++ programs, vol.\u00a0198, pp. 33\u201346 (2008)","DOI":"10.1016\/j.entcs.2007.10.019"},{"issue":"2-3","key":"3_CR24","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-002-0104-3","volume":"5","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. STTT\u00a05(2-3), 247\u2013267 (2004)","journal-title":"STTT"},{"key":"3_CR25","unstructured":"Edelkamp, S., Rensink, A.: Graph transformation and AI planning. In: ICAPS 2007-Workshop on the Knowledge Engineering Competition (2007)"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-642-00431-5_5","volume-title":"Model Checking and Artificial Intelligence","author":"S. Edelkamp","year":"2009","unstructured":"Edelkamp, S., Schuppan, V., Bo\u0161na\u010dki, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS, vol.\u00a05348, pp. 65\u201389. Springer, Heidelberg (2009)"},{"key":"3_CR27","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1613\/jair.1129","volume":"20","author":"M. Fox","year":"2003","unstructured":"Fox, M., Long, D.: PDDL2.1: An extension of pddl for expressing temporal planning domains. JAIR\u00a020, 61\u2013124 (2003)","journal-title":"JAIR"},{"key":"3_CR28","unstructured":"Gerevini, A., Haslum, P., Long, D., Saetti, A., Dimopoulos, Y.: Deterministic planning in the fifth international planning competition: 7pddl3"},{"key":"3_CR29","unstructured":"Gleick, J.: Little bug, big bang. New York Times vom 1\u00a0(Dezember 1996)"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"issue":"4","key":"3_CR31","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/s10009-003-0130-9","volume":"6","author":"A. Groce","year":"2004","unstructured":"Groce, A., Visser, W.: Heuristics for model checking java programs. STTT\u00a06(4), 260\u2013276 (2004)","journal-title":"STTT"},{"key":"3_CR32","unstructured":"Haslum, P., Bonet, B., Geffner, H.: New admissible heuristics for domain-independent planning. In: AAAI, pp. 1163\u20131168 (2005)"},{"issue":"4","key":"3_CR33","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking java programs using JAVA pathfinder. STTT\u00a02(4), 366\u2013381 (2000)","journal-title":"STTT"},{"issue":"1","key":"3_CR34","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/s10009-002-0080-7","volume":"4","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Visser, W.: Program model checking as a new trend. STTT\u00a04(1), 8\u201320 (2002)","journal-title":"STTT"},{"key":"3_CR35","unstructured":"Helmert, M.: Decidability and undecidability results for planning with numerical state variables. In: AIPS, pp. 303\u2013312 (2002)"},{"key":"3_CR36","unstructured":"Helmert, M.: A planning heuristic based on causal graph analysis. In: ICAPS, pp. 161\u2013170 (2004)"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Helmert, M., Domshlak, C.: Landmarks, critical paths and abstractions: What\u2019s the difference anyway? In: ICAPS (2009)","DOI":"10.1609\/icaps.v19i1.13370"},{"key":"3_CR38","unstructured":"Helmert, M., Haslum, P., Hoffmann, J.: Flexible abstraction heuristics for optimal sequential planning. In: ICAPS, pp. 176\u2013183 (2007)"},{"key":"3_CR39","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1613\/jair.1144","volume":"20","author":"J. Hoffmann","year":"2003","unstructured":"Hoffmann, J.: The Metric-FF planning system: Translating ignoring delete lists to numeric state variables. JAIR\u00a020, 291\u2013341 (2003)","journal-title":"JAIR"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Edelkamp, S.: The deterministic part of ipc-4: An overview, vol.\u00a024, pp. 519\u2013579 (2005)","DOI":"10.1613\/jair.1677"},{"issue":"2","key":"3_CR41","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1613\/jair.1982","volume":"26","author":"J. Hoffmann","year":"2006","unstructured":"Hoffmann, J., Edelkamp, S., Thiebaux, S., Englert, R., Liporace, F., Trueg, S.: Engineering benchmarks for planning: the domains used in the deterministic part of IPC-4. JAIR\u00a026(2), 453\u2013541 (2006)","journal-title":"JAIR"},{"key":"3_CR42","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"3_CR43","unstructured":"Kautz, H.A., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search. In: AAAI, pp. 1194\u20131201 (1996)"},{"key":"3_CR44","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1308\/147363505X39437","volume":"87","author":"B. K\u00f6nig","year":"2005","unstructured":"K\u00f6nig, B., Kozioura, V.: Augur - a tool for the analysis of graph transformation systems. Bulletin of the EATCS\u00a087, 126\u2013137 (2005)","journal-title":"Bulletin of the EATCS"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-540-78800-3_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Kupferschmid","year":"2008","unstructured":"Kupferschmid, S., Hoffmann, J., Larsen, K.G.: Fast directed model checking via russian doll abstraction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 203\u2013217. Springer, Heidelberg (2008)"},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-540-24732-6_4","volume-title":"Model Checking Software","author":"P. Leven","year":"2004","unstructured":"Leven, P., Mehler, T., Edelkamp, S.: Directed error detection in C++ with the assembly-level model checker stEAM. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 39\u201356. Springer, Heidelberg (2004)"},{"key":"3_CR47","unstructured":"McDermott, D.: The 1998 AI Planning Competition. AI Magazine\u00a021(2) (2000)"},{"key":"3_CR48","unstructured":"Mehler, T.: Challenges and Applications of Assembly-Level Software Model Checking. PhD thesis, Dortmund University of Technology (2006)"},{"key":"3_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/3-540-46017-9_24","volume-title":"Model Checking Software","author":"P. Merino","year":"2002","unstructured":"Merino, P., del Mar Gallardo, M., Martinez, J., Pimentel, E.: \u03b1SPIN: Extending SPIN with abstraction. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 254\u2013258. Springer, Heidelberg (2002)"},{"key":"3_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11513988_9","volume-title":"Computer Aided Verification","author":"I. Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 82\u201397. Springer, Heidelberg (2005)"},{"key":"3_CR51","volume-title":"The C++ Programming Language","author":"B. Stroustrup","year":"1994","unstructured":"Stroustrup, B.: The C++ Programming Language, 2nd edn. Addison-Wesley Publishing Company, Reading (1994)","edition":"2"},{"issue":"2","key":"3_CR52","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Automated Software Engineering Journal\u00a010(2), 203\u2013232 (2003)","journal-title":"Automated Software Engineering Journal"},{"key":"3_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/11537328_5","volume-title":"Model Checking Software","author":"W. Visser","year":"2005","unstructured":"Visser, W., Mehlitz, P.C.: Model checking programs with Java PathFinder. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, p. 27. Springer, Heidelberg (2005)"},{"key":"3_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-03237-0_8","volume-title":"Static Analysis","author":"M. Wehrle","year":"2009","unstructured":"Wehrle, M., Helmert, M.: The causal graph revisited for directed model checking. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 86\u2013101. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Model Checking and Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20674-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T11:27:30Z","timestamp":1686050850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20674-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642206733","9783642206740"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20674-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}