{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T19:49:40Z","timestamp":1773344980505,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642370359","type":"print"},{"value":"9783642370366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37036-6_25","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:35:55Z","timestamp":1361216155000},"page":"451-471","source":"Crossref","is-referenced-by-count":26,"title":["Counterexample-Guided Precondition Inference"],"prefix":"10.1007","author":[{"given":"Mohamed Nassim","family":"Seghir","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL, pp. 1\u20133 (2002)","DOI":"10.1145\/565816.503274"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: ISSTA, pp. 3\u201314 (2008)","DOI":"10.1145\/1390630.1390634"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Blanc, N., Kroening, D.: Race analysis for SystemC using model checking. In: Proceedings of ICCAD 2008, pp. 356\u2013363. IEEE (2008)","DOI":"10.1109\/ICCAD.2008.4681598"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: PLDI, pp. 46\u201355 (1993)","DOI":"10.1145\/173262.155095"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-28756-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozga","year":"2012","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Deciding Conditional Termination. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 252\u2013266. Springer, Heidelberg (2012)"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL, pp. 289\u2013300 (2009)","DOI":"10.1145\/1594834.1480917"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE, pp. 385\u2013395 (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"25_CR8","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI\u2013C programs using SAT. Formal Methods in System Design (FMSD)\u00a025, 105\u2013127 (2004)","journal-title":"Formal Methods in System Design (FMSD)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., 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, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-70545-1_32","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2008","unstructured":"Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving Conditional Termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 328\u2013340. Springer, Heidelberg (2008)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond Safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 415\u2013418. Springer, Heidelberg (2006)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-18275-4_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 150\u2013168. Springer, Heidelberg (2011)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"25_CR14","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Lab. (2003)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"25_CR16","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., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: a new algorithm for property checking. In: SIGSOFT FSE, pp. 117\u2013127 (2006)","DOI":"10.1145\/1181775.1181790"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/11817963_18","volume-title":"Computer Aided Verification","author":"A. Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Wei, O., Chechik, M.: Yasm: A Software Model-Checker for Verification and Refutation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 170\u2013174. Springer, Heidelberg (2006)"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232\u2013244 (2004)","DOI":"10.1145\/982962.964021"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/565816.503279"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"Ivancic, F., Shlyakhter, I., Gupta, A., Ganai, M.K.: Model checking C programs using F-SOFT. In: ICCD, pp. 297\u2013308 (2005)","DOI":"10.1109\/ICCD.2005.77"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A Practical and Complete Approach to Predicate Refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.L.: Array Abstractions from Proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 193\u2013206. Springer, Heidelberg (2007)"},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-78163-9_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y. Moy","year":"2008","unstructured":"Moy, Y.: Sufficient Preconditions for Modular Assertion Checking. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 188\u2013202. Springer, Heidelberg (2008)"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2007)"},{"key":"25_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11547662_21","volume-title":"Static Analysis","author":"X. Rival","year":"2005","unstructured":"Rival, X.: Understanding the Origin of Alarms in Astr\u00e9e. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 303\u2013319. Springer, Heidelberg (2005)"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Chaudhuri, S., Ivancic, F., Gupta, A.: Dynamic inference of likely data preconditions over predicates by tree learning. In: ISSTA, pp. 295\u2013306 (2008)","DOI":"10.1145\/1390630.1390666"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Taghdiri, M.: Inferring specifications to detect errors in code. In: ASE, pp. 144\u2013153 (2004)","DOI":"10.1109\/ASE.2004.1342732"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37036-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T21:32:34Z","timestamp":1745962354000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37036-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370359","9783642370366"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37036-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}