{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:19:18Z","timestamp":1775053158971,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540696087","type":"print"},{"value":"9783540696117","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/978-3-540-69611-7_16","type":"book-chapter","created":{"date-parts":[[2007,4,26]],"date-time":"2007-04-26T09:40:18Z","timestamp":1177580418000},"page":"245-259","source":"Crossref","is-referenced-by-count":86,"title":["ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Podelski","sequence":"first","affiliation":[]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11799573_14","volume-title":"Logic Programming","author":"E. Albert","year":"2006","unstructured":"Albert, E., Arenas-S\u00e1nchez, P., Puebla, G., Hermenegildo, M.V.: Reduced certificates for abstraction-carrying code. In: Etalle, S., Truszczy\u0144ski, M. (eds.) ICLP 2006. LNCS, vol.\u00a04079. Springer, Heidelberg (2006)"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: PLDI (2001)","DOI":"10.1145\/378795.378846"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46002-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2002","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280. Springer, Heidelberg (2002)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI (2003)","DOI":"10.1145\/781151.781153"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0056604","volume-title":"Principles of Declarative Programming","author":"B. Cui","year":"1998","unstructured":"Cui, B., Dong, Y., Du, X., Kumar, K.N., Ramakrishnan, C.R., Ramakrishnan, I.V., Roychoudhury, A., Smolka, S.A., Warren, D.S.: Logic programming and model checking. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol.\u00a01490. Springer, Heidelberg (1998)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579. Springer, Heidelberg (1999)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Flanagan, C.: Automatic software model checking via constraint logic. Sci. Comput. Program.\u00a050(1-3) (2004)","DOI":"10.1016\/j.scico.2004.01.006"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44802-0","volume-title":"Logic Based Program Synthesis and Transformation","author":"L. Fribourg","year":"2001","unstructured":"Fribourg, L.: Constraint logic programming applied to model checking. In: Lau, K.-K. (ed.) LOPSTR 2000. LNCS, vol.\u00a02042. Springer, Heidelberg (2001)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Heintze, N., Michaylov, S., Stuckey, P., Yap, R.: Meta-programming in CLP(R). J. of Logic Programming\u00a033(3) (1997)","DOI":"10.1016\/S0743-1066(96)00145-8"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)","DOI":"10.1145\/503272.503279"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"16_CR15","unstructured":"Holzbaur, C.: OFAI clp(q,r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna, TR-95-09 (1995)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Ivancic","year":"2005","unstructured":"Ivancic, F., Jain, H., Gupta, A., Ganai, M.K.: Localization and register sharing for predicate abstraction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440. Springer, Heidelberg (2005)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.: Constraint\u00a0logic\u00a0programming. In: POPL (1987)","DOI":"10.1145\/41625.41635"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Jaffar","year":"2005","unstructured":"Jaffar, J., Santosa, A.E., Voicu, R.: A CLP method for compositional and intermittent predicate abstraction. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855. Springer, Heidelberg (2005)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"FM 2005: Formal Methods","author":"M. Leuschel","year":"2005","unstructured":"Leuschel, M., Butler, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582. Springer, Heidelberg (2005)"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11921240_23","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"R. Meyer","year":"2006","unstructured":"Meyer, R., Faber, J., Rybalchenko, A.: Model checking data-expensive real-time systems. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281. Springer, Heidelberg (2006)"},{"key":"16_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44957-4_26","volume-title":"Computational Logic - CL 2000","author":"U. Nilsson","year":"2000","unstructured":"Nilsson, U., L\u00fcbcke, J.: Constraint logic programming for local and symbolic model-checking. In: Palamidessi, C., et al. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861. Springer, Heidelberg (2000)"},{"key":"16_CR22","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation (submitted, 2006)"}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69611-7_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:01:42Z","timestamp":1605762102000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69611-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540696087","9783540696117"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69611-7_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}