{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T04:10:09Z","timestamp":1746418209562,"version":"3.40.4"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319127354"},{"type":"electronic","value":"9783319127361"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12736-1_13","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T14:53:24Z","timestamp":1413212004000},"page":"236-254","source":"Crossref","is-referenced-by-count":7,"title":["Necessary and Sufficient Preconditions via Eager Abstraction"],"prefix":"10.1007","author":[{"given":"Mohamed Nassim","family":"Seghir","sequence":"first","affiliation":[]},{"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Seghir, M.N., Kroening, D.: Counterexample-guided precondition inference. In: Felleisen, M., Gardner, P. (eds.) ESO 2013. LNCS, vol.\u00a07792, pp. 451\u2013471. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_25"},{"key":"13_CR2","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":"13_CR3","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":"13_CR4","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":"13_CR5","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Lab (2003)"},{"key":"13_CR6","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":"13_CR7","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":"13_CR8","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":"13_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.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, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"13_CR10","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":"13_CR11","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":"13_CR12","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":"13_CR13","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":"13_CR14","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., Kroning, 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)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI, pp. 234\u2013245 (2002)","DOI":"10.1145\/543552.512558"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: Vcc: Contract-based modular verification of concurrent c. In: ICSE Companion, pp. 429\u2013430 (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"13_CR18","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":"13_CR19","doi-asserted-by":"crossref","unstructured":"Blanc, N., Kroening, D.: Race analysis for systemc using model checking. ACM Trans. Design Autom. Electr. Syst.\u00a015 (2010)","DOI":"10.1145\/1754405.1754406"},{"key":"13_CR20","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"},{"key":"13_CR21","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":"13_CR22","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":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-35873-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2013","unstructured":"Cousot, P., Cousot, R., F\u00e4hndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 128\u2013148. Springer, Heidelberg (2013)"},{"key":"13_CR24","first-page":"89","volume":"287","author":"A. Min\u00e9","year":"2012","unstructured":"Min\u00e9, A.: Inferring sufficient conditions with backward polyhedral under-approximations. ENTCS\u00a0287, 89\u2013100 (2012)","journal-title":"ENTCS"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Bakhirkin, A., Berdine, J., Piterman, N.: Backward analysis via over-approximate abstraction and under-approximate subtraction. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol.\u00a08723, pp. 34\u201350. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-319-10936-7_3"},{"key":"13_CR26","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":"13_CR27","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\u00c9E. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 303\u2013319. Springer, Heidelberg (2005)"},{"key":"13_CR28","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":"13_CR29","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":"13_CR30","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)"}],"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-319-12736-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T03:47:37Z","timestamp":1746416857000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-12736-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319127354","9783319127361"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12736-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}