{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:55:23Z","timestamp":1770274523737,"version":"3.49.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319662626","type":"print"},{"value":"9783319662633","type":"electronic"}],"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-66263-3_22","type":"book-chapter","created":{"date-parts":[[2017,8,8]],"date-time":"2017-08-08T08:05:11Z","timestamp":1502179511000},"page":"347-363","source":"Crossref","is-referenced-by-count":3,"title":["Theory Refinement for Program Verification"],"prefix":"10.1007","author":[{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sepideh","family":"Asadi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karine","family":"Even-Mendoza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hana","family":"Chockler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,9]]},"reference":[{"key":"22_CR1","unstructured":"http:\/\/verify.inf.usi.ch\/hifrog\/theoref"},{"key":"22_CR2","unstructured":"http:\/\/www.cprover.org\/"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-54580-5_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Alt","year":"2017","unstructured":"Alt, L., Asadi, S., Chockler, H., Even Mendoza, K., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: HiFrog: SMT-based function summarization for software verification. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 207\u2013213. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54580-5_12"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-29613-5_1","volume-title":"Verified Software: Theories, Tools, and Experiments","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). doi: 10.1007\/978-3-319-29613-5_1"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). doi: 10.1007\/3-540-49059-0_14"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-18275-4_7"},{"key":"22_CR7","unstructured":"Brady, B.A., Bryant, R.E., Seshia, S.A.: Learning conditional abstractions. In: Proceedings of FMCAD 2011, pp. 116\u2013124. FMCAD Inc. (2011)"},{"key":"22_CR8","doi-asserted-by":"crossref","first-page":"165","DOI":"10.3233\/SAT190067","volume":"6","author":"R Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. J. Satisfiability Boolean Model. Comput. 6, 165\u2013201 (2009)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-540-73368-3_54","volume-title":"Computer Aided Verification","author":"R Bruttomesso","year":"2007","unstructured":"Bruttomesso, R., et al.: A lazy and layered SMT( $$\\cal{BV}$$ ) solver for hard industrial verification problems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 547\u2013560. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73368-3_54"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-662-54577-5_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2017","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 58\u201375. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54577-5_4"},{"key":"22_CR11","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":"EM 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. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). doi: 10.1007\/10722167_15"},{"issue":"5","key":"22_CR12","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B., Wegman, M., Zadeck, F.: An efficient method of computing static single assignment form. In: Proceedings of POPL 1989, pp. 25\u201335. ACM (1989)","DOI":"10.1145\/75277.75280"},{"issue":"3","key":"22_CR14","doi-asserted-by":"crossref","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":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-642-36742-7_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Fedyukovich","year":"2013","unstructured":"Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: incremental upgrade checker for C. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 292\u2013307. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_21"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-54862-8_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gurfinkel","year":"2014","unstructured":"Gurfinkel, A., Belov, A., Marques-Silva, J.: Synthesizing safe bit-precise invariants. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 93\u2013108. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_7"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"680","DOI":"10.1007\/978-3-319-08867-9_45","volume-title":"Computer Aided Verification","author":"L Hadarean","year":"2014","unstructured":"Hadarean, L., Bansal, K., Jovanovi\u0107, D., Barrett, C., Tinelli, C.: A tale of two solvers: eager and lazy approaches to bit-vectors. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 680\u2013695. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_45"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Ho, Y.S., Chauhan, P., Roy, P., Mishchenko, A., Brayton, R.: Efficient uninterpreted function abstraction and refinement for word-level model checking. In: Proceedings of FMCAD 2016, pp. 65\u201372. ACM (2016)","DOI":"10.1109\/FMCAD.2016.7886662"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-319-40970-2_35","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","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). doi: 10.1007\/978-3-319-40970-2_35"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Harel, D.: Theory-aided model checking of concurrent transition systems. In: Proceedings of FMCAD 2015, pp. 81\u201388. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542256"},{"key":"22_CR21","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-50497-0","volume-title":"Decision Procedures - An Algorithmic Point of View","author":"D Kroening","year":"2016","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, 2nd edn. Springer, Heidelberg (2016)","edition":"2"},{"issue":"1","key":"22_CR22","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10009-015-0389-7","volume":"18","author":"T Kutsuna","year":"2016","unstructured":"Kutsuna, T., Ishii, Y., Yamamoto, A.: Abstraction and refinement of mathematical functions toward SMT-based test-case generation. Int. J. Softw. Tools Technol. Transf. 18(1), 109\u2013120 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"22_CR23","doi-asserted-by":"crossref","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."}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66263-3_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,14]],"date-time":"2020-10-14T11:54:39Z","timestamp":1602676479000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66263-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662626","9783319662633"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66263-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}