{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T18:00:12Z","timestamp":1725732012016},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642388552"},{"type":"electronic","value":"9783642388569"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38856-9_22","type":"book-chapter","created":{"date-parts":[[2013,6,15]],"date-time":"2013-06-15T04:05:28Z","timestamp":1371269128000},"page":"412-432","source":"Crossref","is-referenced-by-count":14,"title":["Interpolation-Based Verification of Floating-Point Programs with Abstract CDCL"],"prefix":"10.1007","author":[{"given":"Martin","family":"Brain","sequence":"first","affiliation":[]},{"given":"Vijay","family":"D\u2019Silva","sequence":"additional","affiliation":[]},{"given":"Alberto","family":"Griggio","sequence":"additional","affiliation":[]},{"given":"Leopold","family":"Haller","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-35873-9_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Brain","year":"2013","unstructured":"Brain, M., D\u2019Silva, V., Haller, L., Griggio, A., Kroening, D.: An abstract interpretation of DPLL(T). In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 455\u2013475. Springer, Heidelberg (2013)"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Brillout, A., Kroening, D., Wahl, T.: Mixed abstractions for floating-point arithmetic. In: Proc.\u00a0of Formal Methods in Computer-Aided Design, pp. 69\u201376. IEEE Computer Society Press (2009)","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-31424-7_23","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2012","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 277\u2013293. Springer, Heidelberg (2012)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 93\u2013107. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"issue":"1","key":"22_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/1838552.1838559","volume":"12","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Transactions on Computational Logic\u00a012(1), 7 (2010)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"2-3","key":"22_CR6","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1023\/B:FORM.0000040025.89719.f3","volume":"25","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Formal Methods in Systems Design\u00a025(2-3), 105\u2013127 (2004)","journal-title":"Formal Methods in Systems Design"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-04570-7_6","volume-title":"Formal Methods for Industrial Critical Systems","author":"D. Delmas","year":"2009","unstructured":"Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., V\u00e9drine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol.\u00a05825, pp. 53\u201369. Springer, Heidelberg (2009)"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: Proc.\u00a0of Principles of Programming Languages, pp. 143\u2013154 (2013)","DOI":"10.1145\/2480359.2429087"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Proc.\u00a0of Tools and Algorithms for the Construction and Analysis of Systems, pp. 48\u201363 (2012)","DOI":"10.1007\/978-3-642-28756-5_5"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Garoche, P.-L., Kahsai, T., Tinelli, C.: Invariant stream generators using automatic abstract transformers based on a decidable logic. CoRR, abs\/1205.3758 (2012)","DOI":"10.1007\/978-3-642-38088-4_10"},{"key":"22_CR12","unstructured":"Griggio, A.: Effective word-level interpolation for software verification. In: Proc.\u00a0of Formal Methods in Computer-Aided Design (2011)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-78800-3_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2008","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 443\u2013458. Springer, Heidelberg (2008)"},{"key":"22_CR14","unstructured":"Haller, L., Griggio, A., Brain, M., Kroening, D.: Deciding floating-point logic with systematic abstraction. In: Proc.\u00a0of Formal Methods in Computer-Aided Design, pp. 131\u2013140 (2012)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 199\u2013213. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_17"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Kroening, D., Weissenbacher, G.: Lifting propositional interpolants to the word-level. In: FMCAD, pp. 85\u201389. IEEE (2007)","DOI":"10.1109\/FMCAD.2007.4401986"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-642-22110-1_45","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2011","unstructured":"Kroening, D., Weissenbacher, G.: Interpolation-based software verification with Wolverine. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 573\u2013578. Springer, Heidelberg (2011)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"issue":"1","key":"22_CR19","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theoretical Computer Science\u00a0345(1), 101\u2013121 (2005)","journal-title":"Theoretical Computer Science"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: LPAR-18 2012, pp. 123\u2013136. Springer (2006)","DOI":"10.1007\/11817963_14"},{"key":"22_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4705-6","volume-title":"Handbook of Floating-Point Arithmetic","author":"J.-M. Muller","year":"2010","unstructured":"Muller, J.-M., Brisebarre, N., de Dinechin, F., Jeannerod, C.-P., Lef\u00e8vre, V., Melquiond, G., Revol, N., Stehl\u00e9, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkh\u00e4user, Boston (2010)"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-33558-7_43","volume-title":"Principles and Practice of Constraint Programming","author":"O. Ponsini","year":"2012","unstructured":"Ponsini, O., Michel, C., Rueher, M.: Refining abstract interpretation based value analysis with constraint programming techniques. In: Milano, M. (ed.) CP 2012. LNCS, vol.\u00a07514, pp. 593\u2013607. Springer, Heidelberg (2012)"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. In: Proc.\u00a0of Principles of Programming Languages, pp. 537\u2013548. ACM Press (2013)","DOI":"10.1145\/2480359.2429132"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Truchet, C., Pelleau, M., Benhamou, F.: Abstract domains for constraint programming, with the example of octagons. In: Symbolic and Numeric Algorithms for Scientific Computing, pp. 72\u201379 (2010)","DOI":"10.1109\/SYNASC.2010.69"},{"key":"22_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/3-540-45620-1_26","volume-title":"Automated Deduction - CADE-18","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The quest for efficient Boolean satisfiability solvers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 295\u2013313. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38856-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,25]],"date-time":"2022-02-25T08:36:37Z","timestamp":1645778197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38856-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388552","9783642388569"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38856-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}