{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:11:40Z","timestamp":1773655900044,"version":"3.50.1"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319336923","type":"print"},{"value":"9783319336930","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-33693-0_2","type":"book-chapter","created":{"date-parts":[[2016,5,24]],"date-time":"2016-05-24T05:35:47Z","timestamp":1464068147000},"page":"20-27","source":"Crossref","is-referenced-by-count":6,"title":["Symbolic Computation and Automated Reasoning for Program Analysis"],"prefix":"10.1007","author":[{"given":"Laura","family":"Kov\u00e1cs","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,5,24]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/978-3-662-48899-7_30","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"W Ahrendt","year":"2015","unstructured":"Ahrendt, W., Kov\u00e1cs, L., Robillard, S.: Reasoning About Loops Using Vampire in KeY. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 434\u2013443. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48899-7_30"},{"issue":"3\u20134","key":"2_CR2","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1016\/j.jsc.2005.09.007","volume":"41","author":"B Buchberger","year":"2006","unstructured":"Buchberger, B.: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. J. Symbolic Comput. 41(3\u20134), 475\u2013511 (2006)","journal-title":"J. Symbolic Comput."},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","first-page":"52","volume-title":"Logic of Programs","author":"EM Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs. LNCS, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) ATFL. LNCS, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"2_CR5","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: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/978-3-642-38574-2_12","volume-title":"Automated Deduction \u2013 CADE-24","author":"L Moura de","year":"2013","unstructured":"de Moura, L., Passmore, G.O.: Computation in real closed infinitesimal and transcendental extensions of the rationals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 178\u2013192. Springer, Heidelberg (2013)"},{"key":"2_CR7","unstructured":"de Moura, L.M., Bjorner, N.: Proofs and refutations, and z3. In: CEUR Workshop Proceedings (2008)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Hamon, G., de Moura, L., Rushby, J.M.: Generating efficient test sets with a model checker. In: SEFM, pp. 261\u2013270 (2004)","DOI":"10.1109\/SEFM.2004.1347530"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 3920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Kotelnikov, E., Kov\u00e1cs, L., Reger, G., Voronkov, A.: The Vampire and the FOOL. In: Proceedings of CPP, pp. 37\u201348. ACM (2016)","DOI":"10.1145\/2854065.2854071"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/978-3-540-78800-3_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Kov\u00e1cs","year":"2008","unstructured":"Kov\u00e1cs, L.: Reasoning algebraically about P-solvable loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 249\u2013264. Springer, Heidelberg (2008)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/978-3-642-11486-1_21","volume-title":"Perspectives of Systems Informatics","author":"L Kov\u00e1cs","year":"2010","unstructured":"Kov\u00e1cs, L.: A complete invariant generation approach for P-solvable loops. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 242\u2013256. Springer, Heidelberg (2010)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413\u2013427. Springer, Heidelberg (2008)"},{"issue":"2","key":"2_CR16","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"key":"2_CR17","volume-title":"Handbook of Automated Reasoning (in 2 Volumes)","author":"JA Robinson","year":"2001","unstructured":"Robinson, J.A., Voronkov, A.: Handbook of Automated Reasoning (in 2 Volumes). Elsevier and MIT Press, Cambridge (2001)"},{"key":"2_CR18","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0304-3975(82)90067-6","volume":"18","author":"J Sifakis","year":"1982","unstructured":"Sifakis, J.: A unified approach for studying the properties of transition systems. Theor. Comput. Sci. 18, 227\u2013258 (1982)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33693-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T14:43:49Z","timestamp":1498315429000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33693-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319336923","9783319336930"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33693-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}