{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T07:48:51Z","timestamp":1771573731996,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540697350","type":"print"},{"value":"9783540697381","type":"electronic"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-69738-1_27","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T12:58:07Z","timestamp":1194872287000},"page":"378-394","source":"Crossref","is-referenced-by-count":64,"title":["Invariant Synthesis for Combined Theories"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","first-page":"1","volume-title":"Proc. POPL","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL, pp. 1\u20133. ACM, New York (2002)"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"key":"27_CR3","volume-title":"Model Theory","author":"C.C. Chang","year":"1990","unstructured":"Chang, C.C., Keisler, H.J.: Model Theory, 3rd edn. North-Holland, Amsterdam (1990)","edition":"3"},{"key":"27_CR4","first-page":"134","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages, pp. 134\u2013183. Springer, New York (1975)"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b105073","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, Springer, Heidelberg (2005)"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol.\u00a0631, pp. 269\u2013295. Springer, Heidelberg (1992)"},{"key":"27_CR8","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"Proc. PLDI","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., et al.: Extended static checking for Java. In: Proc. PLDI, pp. 234\u2013245. ACM, New York (2002)"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, pp. 19\u201332. AMS (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"27_CR10","doi-asserted-by":"crossref","first-page":"376","DOI":"10.1145\/1133981.1134026","volume-title":"Proc. PLDI","author":"S. Gulwani","year":"2006","unstructured":"Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Proc. PLDI, pp. 376\u2013386. ACM, New York (2006)"},{"key":"27_CR11","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"Proc. POPL","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., et al.: Lazy abstraction. In: Proc. POPL, pp. 58\u201370. ACM, New York (2002)"},{"key":"27_CR12","unstructured":"Holzbaur, C.: OFAI clp(q,r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna. TR-95-09 (1995)"},{"key":"27_CR13","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Proc. Deduction and Applications, vol. 05431. IBFI Schloss Dagstuhl (2006)"},{"key":"27_CR14","unstructured":"Kapur, D., Zarba, C.: A reduction approach to decision procedures. Technical Report TR-CS-2005-44, University of New Mexico (2005)"},{"key":"27_CR15","unstructured":"Laboratory, T.I.S.: SICStus Prolog User\u2019s Manual. Swedish Institute of Computer Science, PO Box 1263 SE-164 29 Kista, Sweden. Release 3.8.7 (October 2001)"},{"key":"27_CR16","doi-asserted-by":"crossref","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":"27_CR17","first-page":"21","volume-title":"Proc. IFIP Congress","author":"J. McCarthy","year":"1962","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Proc. IFIP Congress, pp. 21\u201328. North-Holland, Amsterdam (1962)"},{"key":"27_CR18","unstructured":"Nelson, G.: Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center (1981)"},{"key":"27_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"Static Analysis","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 53\u201368. Springer, Heidelberg (2004)"},{"key":"27_CR20","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1145\/964001.964028","volume-title":"Proc. POPL","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: Proc. POPL, pp. 318\u2013329. ACM, New York (2004)"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a03385, pp. 25\u201341. Springer, Heidelberg (2005)"},{"key":"27_CR22","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)"},{"key":"27_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,14]],"date-time":"2023-05-14T17:49:25Z","timestamp":1684086565000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540697350","9783540697381"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007]]}}}