{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T11:40:32Z","timestamp":1693050032661},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,8,5]],"date-time":"2021-08-05T00:00:00Z","timestamp":1628121600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,8,5]],"date-time":"2021-08-05T00:00:00Z","timestamp":1628121600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Universit\u00e0 della Svizzera italiana"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,2]]},"abstract":"Abstract<\/jats:title>The use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states, e.g. as candidates for inductive loop invariants. Interpolants for a linear system can be efficiently computed from a Simplex refutation by applying the Farkas\u2019 lemma. However, these interpolants do not always suit the verification task\u2014in the worst case, they can even prevent the verification algorithm from converging. This work introduces the decomposed interpolants, a fundamental extension of the Farkas interpolants, obtained by identifying and separating independent components from the interpolant structure, using methods from linear algebra. We also present an efficient polynomial algorithm to compute decomposed interpolants and analyse its properties. We experimentally show that the use of decomposed interpolants in model checking results in immediate convergence on instances where state-of-the-art approaches diverge. Moreover, since being based on the efficient Simplex method, the approach is very competitive in general.<\/jats:p>","DOI":"10.1007\/s10009-021-00641-z","type":"journal-article","created":{"date-parts":[[2021,8,5]],"date-time":"2021-08-05T16:03:45Z","timestamp":1628179425000},"page":"111-125","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Using linear algebra in decomposition of Farkas interpolants"],"prefix":"10.1007","volume":"24","author":[{"given":"Martin","family":"Blicha","sequence":"first","affiliation":[]},{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Kofro\u0148","sequence":"additional","affiliation":[]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,8,5]]},"reference":[{"key":"641_CR1","first-page":"313","volume-title":"CAV 2013, LNCS","author":"A Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina, N., Veith, H. (eds.) CAV 2013, LNCS, vol. 8044, pp. 313\u2013329. Springer, Heidelberg (2013)"},{"key":"641_CR2","first-page":"1","volume-title":"VSTTE 2015, LNCS","author":"L Alt","year":"2016","unstructured":"Alt, L., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: A proof-sensitive approach for small propositional interpolants. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015, LNCS, vol. 9593, pp. 1\u201318. Springer, Cham (2016)"},{"key":"641_CR3","doi-asserted-by":"crossref","unstructured":"Alt, L., Hyv\u00e4rinen, A.E.J., Asadi, S., Sharygina, N.: Duality-based interpolation for quantifier-free equalities and uninterpreted functions. In: Stewart, D., Weissenbacher, G. (eds.) FMCAD 2017, pp. 39\u201346. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102239"},{"key":"641_CR4","doi-asserted-by":"crossref","unstructured":"Alt, L., Hyv\u00e4rinen, A.E.J., Sharygina, N.: LRA interpolants from no man\u2019s land. In: Strichman, O., Tzoref-Brill, R. (eds.) HVC 2017, LNCS, vol. 10629, pp. 195\u2013210. Springer, Cham (2017)","DOI":"10.1007\/978-3-319-70389-3_13"},{"key":"641_CR5","volume-title":"Elementary Linear Algebra","author":"S Andrilli","year":"2016","unstructured":"Andrilli, S., Hecker, D.: Elementary Linear Algebra, 5th edn. Academic Press, Cambridge (2016)","edition":"5"},{"key":"641_CR6","doi-asserted-by":"crossref","unstructured":"Barrett, C., de\u00a0Moura, L.M., Ranise, S., Stump, A., Tinelli, C.: The SMT-LIB initiative and the rise of SMT. In: Barner, S., Harris, I.G., Kroening, D., Raz, O. (eds.) HVC 2010 LNCS, vol. 6504, p.\u00a03. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-19583-9_2"},{"key":"641_CR7","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories, Frontiers in Artificial Intelligence and Applications, 1st edition. vol. 185, pp. 825\u2013885 (2009)"},{"key":"641_CR8","doi-asserted-by":"publisher","unstructured":"Blicha, M., Hyv\u00e4rinen, A.E.J., Kofro\u0148, J., Sharygina, N.: Decomposing Farkas interpolants. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, p. 3\u201320. Springer International Publishing, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_1","DOI":"10.1007\/978-3-030-17462-0_1"},{"key":"641_CR9","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D.A. (eds.) VMCAI 2011, LNCS, vol. 6538, pp. 70\u201387. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"641_CR10","first-page":"1","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2012","author":"AR Bradley","year":"2012","unstructured":"Bradley, A.R.: Understanding IC3. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing - SAT 2012, pp. 1\u201314. Springer, Berlin Heidelberg (2012)"},{"issue":"1","key":"641_CR11","doi-asserted-by":"publisher","first-page":"7:1","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 Trans. Comput. Logic 12(1), 7:1\u20137:54 (2010)","journal-title":"ACM Trans. Comput. Logic"},{"issue":"3","key":"641_CR12","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Logic 22(3), 269\u2013285 (1957)","journal-title":"J. Symb. Logic"},{"issue":"7","key":"641_CR13","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"641_CR14","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"issue":"3","key":"641_CR15","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"641_CR16","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: VMCAI 2010. LNCS, vol. 5944, pp. 129\u2013145. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"641_CR17","first-page":"737","volume-title":"CAV 2014, LNCS","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014, LNCS, vol. 8559, pp. 737\u2013744. Springer, Berlin (2014)"},{"key":"641_CR18","first-page":"81","volume-title":"CAV 2006, LNCS","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006, LNCS, vol. 4144, pp. 81\u201394. Springer, Berlin (2006)"},{"key":"641_CR19","unstructured":"Farkas, G.: A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian) [On the applications of the mechanical principle of Fourier] (1894)"},{"key":"641_CR20","first-page":"343","volume-title":"CAV 2015, LNCS","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015)"},{"key":"641_CR21","first-page":"255","volume-title":"ATVA 2013","author":"A Gurfinkel","year":"2013","unstructured":"Gurfinkel, A., Rollini, S.F., Sharygina, N.: Interpolation properties and SAT-based model checking. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013, pp. 255\u2013271. Springer, Cham (2013)"},{"issue":"5296","key":"641_CR22","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1126\/science.275.5296.51","volume":"275","author":"BA Huberman","year":"1997","unstructured":"Huberman, B.A., Lukose, R.M., Hogg, T.: An economics approach to hard computational problems. Science 275(5296), 51\u201354 (1997)","journal-title":"Science"},{"key":"641_CR23","first-page":"547","volume-title":"SAT 2016, LNCS","author":"AEJ Hyv\u00e4rinen","year":"2016","unstructured":"Hyv\u00e4rinen, A.E.J., Marescotti, M., Alt, L., Sharygina, N.: OpenSMT2: An SMT solver for multi-core and cloud computing. In: Creignou, N., Le Berre, D. (eds.) SAT 2016, LNCS, vol. 9710, pp. 547\u2013553. Springer, Cham (2016)"},{"key":"641_CR24","volume-title":"FASE 2016","author":"P Jan\u010d\u00edk","year":"2016","unstructured":"Jan\u010d\u00edk, P., Alt, L., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Kofro\u0148, J., Sharygina, N.: PVAIR: Partial variable assignment interpolator. In: Stevens, P., Wasowski, A. (eds.) FASE 2016. Springer, Heidelberg (2016)"},{"key":"641_CR25","doi-asserted-by":"crossref","unstructured":"Jan\u010d\u00edk, P., Kofro\u0148, J., Rollini, S.F., Sharygina, N.: On interpolants and variable assignments. In: FMCAD 2014, pp. 123\u2013130. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987604"},{"key":"641_CR26","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Dutertre, B.: Property-directed k-induction. In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp. 85\u201392 (2016)","DOI":"10.1109\/FMCAD.2016.7886665"},{"key":"641_CR27","first-page":"17","volume-title":"CAV 2014","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014, pp. 17\u201334. Springer, Cham (2014)"},{"key":"641_CR28","first-page":"509","volume-title":"CP 2009","author":"K Korovin","year":"2009","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I.P. (ed.) CP 2009, pp. 509\u2013523. Springer, Heidelberg (2009)"},{"key":"641_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)"},{"key":"641_CR30","first-page":"1","volume-title":"CAV 2013","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2013, pp. 1\u201313. Springer, Heidelberg (2003)"},{"issue":"1","key":"641_CR31","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"641_CR32","first-page":"453","volume-title":"RTA 2005, LNCS","author":"R Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Giesl, J. (ed.) RTA 2005, LNCS, vol. 3467, pp. 453\u2013468. Springer, Berlin (2005)"},{"issue":"3","key":"641_CR33","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Logic 62(3), 981\u2013998 (1997)","journal-title":"J. Symb. Logic"},{"key":"641_CR34","first-page":"683","volume-title":"LPAR 2013, LNCS","author":"SF Rollini","year":"2013","unstructured":"Rollini, S.F., Alt, L., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: PeRIPLO: a framework for producing effective interpolants in SAT-based software verification. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013, LNCS, vol. 8312, pp. 683\u2013693. Springer, Heidelberg (2013)"},{"key":"641_CR35","doi-asserted-by":"crossref","unstructured":"Rollini, S.F., \u0160er\u00fd, O., Sharygina, N.: Leveraging interpolant strength in model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012, LNCS, vol. 7358, pp. 193\u2013209. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-31424-7_18"},{"key":"641_CR36","first-page":"346","volume-title":"VMCAI 2007, LNCS","author":"A Rybalchenko","year":"2007","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007, LNCS, vol. 4349, pp. 346\u2013362. Springer, Heidelberg (2007)"},{"key":"641_CR37","first-page":"495","volume-title":"VMCAI 2018","author":"T Schindler","year":"2018","unstructured":"Schindler, T., Jovanovi\u0107, D.: Selfless interpolation for infinite-state model checking. In: Dillig, I., Palsberg, J. (eds.) VMCAI 2018, pp. 495\u2013515. Springer, Cham (2018)"},{"key":"641_CR38","doi-asserted-by":"crossref","unstructured":"Scholl, C., Pigorsch, F., Disch, S., Althaus, E.: Simple interpolants for linear arithmetic. In: DATE 2014, pp. 1\u20136. IEEE (2014)","DOI":"10.7873\/DATE.2014.128"},{"key":"641_CR39","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1998","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons Inc, New York (1998)"},{"key":"641_CR40","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: Incremental upgrade checking by means of interpolation-based function summaries. In: 2012 Formal Methods in Computer-Aided Design (FMCAD), pp. 114\u2013121 (2012)"},{"key":"641_CR41","first-page":"127","volume-title":"FMCAD 2000","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Hunt, W.A., Johnson, S.D. (eds.) FMCAD 2000, pp. 127\u2013144. Springer, Heidelberg (2000)"},{"issue":"5","key":"641_CR42","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JPM Silva","year":"1999","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00641-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00641-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00641-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T16:16:51Z","timestamp":1647361011000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00641-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,5]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["641"],"URL":"http:\/\/dx.doi.org\/10.1007\/s10009-021-00641-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,5]]},"assertion":[{"value":"20 July 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 August 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}
