{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:41Z","timestamp":1763468141048},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642380877"},{"type":"electronic","value":"9783642380884"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38088-4_10","type":"book-chapter","created":{"date-parts":[[2013,5,8]],"date-time":"2013-05-08T20:38:27Z","timestamp":1368045507000},"page":"139-154","source":"Crossref","is-referenced-by-count":15,"title":["Incremental Invariant Generation Using Logic-Based Automatic Abstract Transformers"],"prefix":"10.1007","author":[{"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"first","affiliation":[]},{"given":"Temesghen","family":"Kahsai","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Aspic website, \n                    \n                      http:\/\/laure.gonnord.org\/pro\/aspic\/benchmarks.html"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-44898-5_19","volume-title":"Static Analysis","author":"R. Bagnara","year":"2003","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 337\u2013354. Springer, Heidelberg (2003)"},{"key":"10_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: SMT (2010)"},{"key":"10_CR4","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":"10_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTRE\u00c9 Analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-19805-2_31","volume-title":"Foundations of Software Science and Computational Structures","author":"P. Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Mauborgne, L.: The reduced product of abstract domains and the combination of decision procedures. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol.\u00a06604, pp. 456\u2013472. Springer, Heidelberg (2011)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press (2001)","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"10_CR9","unstructured":"Fast website, \n                    \n                      http:\/\/www.lsv.ens-cachan.fr\/fast\/"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-642-19718-5_13","volume-title":"Programming Languages and Systems","author":"T.M. Gawlitza","year":"2011","unstructured":"Gawlitza, T.M., Monniaux, D.: Improving strategies via SMT solving. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 236\u2013255. Springer, Heidelberg (2011)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/11823230_10","volume-title":"Static Analysis","author":"L. Gonnord","year":"2006","unstructured":"Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 144\u2013160. Springer, Heidelberg (2006)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D. Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 452\u2013466. Springer, Heidelberg (2006)"},{"issue":"6","key":"10_CR13","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/s10009-010-0162-x","volume":"12","author":"A. Gurfinkel","year":"2010","unstructured":"Gurfinkel, A., Chaki, S.: Combining predicate and numeric abstraction for software model checking. STTT\u00a012(6), 409\u2013427 (2010)","journal-title":"STTT"},{"key":"10_CR14","unstructured":"Halbwachs, N.: D\u00e9termination automatique de relations lin\u00e9aires v\u00e9rifi\u00e9es par les variables d\u2019un programme. PhD thesis, University of Grenoble (1979)"},{"issue":"9","key":"10_CR15","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data-flow programming language LUSTRE. Proceedings of the IEEE\u00a079(9), 1305\u20131320 (1991)","journal-title":"Proceedings of the IEEE"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-48294-6_3","volume-title":"Static Analysis","author":"B. Jeannet","year":"1999","unstructured":"Jeannet, B., Halbwachs, N., Raymond, P.: Dynamic partitioning in analyses of numerical properties. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, pp. 39\u201350. Springer, Heidelberg (1999)"},{"key":"10_CR17","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.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/978-3-642-28891-3_35","volume-title":"NASA Formal Methods","author":"T. Kahsai","year":"2012","unstructured":"Kahsai, T., Garoche, P.-L., Tinelli, C., Whalen, M.: Incremental verification with mode variable invariants in state machines. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 388\u2013402. Springer, Heidelberg (2012)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-642-20398-5_15","volume-title":"NASA Formal Methods","author":"T. Kahsai","year":"2011","unstructured":"Kahsai, T., Ge, Y., Tinelli, C.: Instantiation-based invariant discovery. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 192\u2013206. Springer, Heidelberg (2011)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Kahsai, T., Tinelli, C.: PKIND: a parallel k-induction based model checker. In: PDMC. EPTCS, vol.\u00a072, pp. 55\u201362 (2011)","DOI":"10.4204\/EPTCS.72.6"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-11319-2_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. King","year":"2010","unstructured":"King, A., S\u00f8ndergaard, H.: Automatic abstraction for congruences. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 197\u2013213. Springer, Heidelberg (2010)"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Automatic modular abstractions for linear constraints. In: POPL, pp. 140\u2013151. ACM (2009)","DOI":"10.1145\/1594834.1480899"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-23702-7_27","volume-title":"Static Analysis","author":"D. Monniaux","year":"2011","unstructured":"Monniaux, D., Gonnord, L.: Using bounded model checking to focus fixpoint iterations. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 369\u2013385. Springer, Heidelberg (2011)"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"issue":"2","key":"10_CR25","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.entcs.2010.09.018","volume":"267","author":"P. Roux","year":"2010","unstructured":"Roux, P., Delmas, R., Garoche, P.-L.: SMT-AI: an abstract interpreter as oracle for k-induction. Electr. Notes Theor. Comput. Sci.\u00a0267(2), 55\u201368 (2010)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"10_CR26","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.entcs.2010.09.009","volume":"267","author":"P. Schrammel","year":"2010","unstructured":"Schrammel, P., Jeannet, B.: Extending abstract acceleration methods to data-flow programs with numerical inputs. Electr. Notes Theor. Comput. Sci.\u00a0267(1), 101\u2013114 (2010)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-33125-1_10","volume-title":"Static Analysis","author":"A. Thakur","year":"2012","unstructured":"Thakur, A., Elder, M., Reps, T.: Bilateral algorithms for symbolic abstraction. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 111\u2013128. Springer, Heidelberg (2012)"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-31424-7_17","volume-title":"Computer Aided Verification","author":"A. Thakur","year":"2012","unstructured":"Thakur, A., Reps, T.: A method for symbolic computation of abstract operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 174\u2013192. Springer, Heidelberg (2012)"},{"key":"10_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-73595-3_11","volume-title":"Automated Deduction \u2013 CADE-21","author":"A. Tiwari","year":"2007","unstructured":"Tiwari, A., Gulwani, S.: Logical interpretation: Static program analysis using theorem proving. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 147\u2013166. Springer, Heidelberg (2007)"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/978-3-540-24730-2_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Yorsh","year":"2004","unstructured":"Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 530\u2013545. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38088-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T19:49:10Z","timestamp":1557690550000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38088-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642380877","9783642380884"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38088-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}