{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T06:02:24Z","timestamp":1743055344778,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319681665"},{"type":"electronic","value":"9783319681672"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-68167-2_21","type":"book-chapter","created":{"date-parts":[[2017,9,25]],"date-time":"2017-09-25T23:50:53Z","timestamp":1506383453000},"page":"307-326","source":"Crossref","is-referenced-by-count":3,"title":["Lifting CDCL to Template-Based Abstract Domains for Program Verification"],"prefix":"10.1007","author":[{"given":"Rajdeep","family":"Mukherjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leopold","family":"Haller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"Melham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,27]]},"reference":[{"key":"21_CR1","unstructured":"Astr\u00e9e. https:\/\/www.absint.com\/astree\/index.htm"},{"key":"21_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"21_CR3","volume-title":"Handbook of Satisfiability","author":"A Biere","year":"2009","unstructured":"Biere, A., Heule, M., Van Maaren, H., Walsh, T.: Handbook of Satisfiability. IOS, Amsterdam (2009)"},{"key":"21_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: Programming Language Design and Implementation (PLDI), pp. 196\u2013207. ACM (2003)","DOI":"10.1145\/781131.781153"},{"issue":"2","key":"21_CR5","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10703-013-0203-7","volume":"45","author":"M Brain","year":"2014","unstructured":"Brain, M., D\u2019Silva, V., Griggio, A., Haller, L., Kroening, D.: Deciding floating-point logic with abstract conflict driven clause learning. Form. Methods Syst. Des. 45(2), 213\u2013245 (2014)","journal-title":"Form. Methods Syst. Des."},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-662-48288-9_9","volume-title":"Static Analysis","author":"M Brain","year":"2015","unstructured":"Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by k-invariants and k-induction. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 145\u2013161. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48288-9_9"},{"key":"21_CR7","unstructured":"CBMC. http:\/\/www.cprover.org\/cbmc\/"},{"key":"21_CR8","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., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24730-2_15"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-15297-9_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Cotton","year":"2010","unstructured":"Cotton, S.: Natural domain SMT: a preliminary assessment. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 77\u201391. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15297-9_8"},{"key":"21_CR10","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: Principles of Programming Languages (POPL), pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Principles of Programming Languages (POPL), pp. 269\u2013282. ACM (1979)","DOI":"10.1145\/567752.567778"},{"key":"21_CR12","unstructured":"CPROVER verification framework. http:\/\/www.cprover.org\/"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: Principles of Programming Languages (POPL), pp. 143\u2013154. ACM (2013)","DOI":"10.1145\/2429069.2429087"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-28756-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D., Tautschnig, M.: Numeric bounds analysis with conflict-driven learning. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 48\u201363. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_5"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33125-1_22","volume-title":"Static Analysis","author":"V D\u2019Silva","year":"2012","unstructured":"D\u2019Silva, V., Haller, L., Kroening, D.: Satisfiability solvers are static analysers. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 317\u2013333. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33125-1_22"},{"key":"21_CR16","first-page":"209","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J. Satisf. Boolean Model. Comput. 1, 209\u2013236 (2007)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"21_CR17","unstructured":"Haller, L.C.R.: Abstract satisfaction. Ph.D. thesis, University of Oxford, UK (2013)"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Harris, W.R., Sankaranarayanan, S., Ivan\u010di\u0107, F., Gupta, A.: Program analysis via satisfiability modulo path programs. In: Principles of Programming Languages (POPL), pp. 71\u201382. ACM (2010)","DOI":"10.1145\/1706299.1706309"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_52"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-642-02658-4_35","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2009","unstructured":"McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 462\u2013476. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_35"},{"key":"21_CR21","unstructured":"MiniSAT. http:\/\/minisat.se\/"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Moura de","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35873-9_1"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Mukherjee, R., Schrammel, P., Haller, L., Kroening, D., Melham, T.: Lifting CDCL to template-based abstract domains for program verification (extended version). arXiv Computing Research Repository [cs.LO], July 2017. arXiv:1707.02011","DOI":"10.1007\/978-3-319-68167-2_21"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1007\/978-3-662-49674-9_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Mukherjee","year":"2016","unstructured":"Mukherjee, R., Tautschnig, M., Kroening, D.: v2c \u2013 A verilog to C translator. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 580\u2013586. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_38"},{"issue":"5","key":"21_CR25","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X Rival","year":"2007","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM TOPLAS 29(5), 26 (2007)","journal-title":"ACM TOPLAS"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25\u201341. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-30579-8_2"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1007\/978-3-662-49674-9_56","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Schrammel","year":"2016","unstructured":"Schrammel, P., Kroening, D.: 2LS for program analysis. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 905\u2013907. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_56"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68167-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T19:38:15Z","timestamp":1570131495000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68167-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319681665","9783319681672"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68167-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}