{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T06:59:54Z","timestamp":1774594794738,"version":"3.50.1"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,12,5]],"date-time":"2007-12-05T00:00:00Z","timestamp":1196812800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2008,2]]},"DOI":"10.1007\/s10703-007-0046-1","type":"journal-article","created":{"date-parts":[[2007,12,6]],"date-time":"2007-12-06T16:12:06Z","timestamp":1196957526000},"page":"25-55","source":"Crossref","is-referenced-by-count":66,"title":["Constructing invariants for hybrid systems"],"prefix":"10.1007","volume":"32","author":[{"given":"Sriram","family":"Sankaranarayanan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henny B.","family":"Sipma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zohar","family":"Manna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,12,5]]},"reference":[{"key":"46_CR1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Proc 14th international conference on computer aided verification","author":"E Asarin","year":"2002","unstructured":"Asarin E, Dang T, Maler O (2002) The d\/dt tool for verification of hybrid systems. In: Proc 14th international conference on computer aided verification. LNCS, vol 2404. Springer, Berlin, pp 365\u2013370"},{"key":"46_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term rewriting and all that","author":"F Baader","year":"1998","unstructured":"Baader F, Nipkow T (1998) Term rewriting and all that. Cambridge University Press, Cambridge"},{"key":"46_CR3","series-title":"LNCS","first-page":"232","volume-title":"Proc of workshop on verification and control of hybrid systems III. Oct 1995","author":"J Bengtsson","year":"1995","unstructured":"Bengtsson J, Larsen KG, Larsson F, Pettersson P, Yi W (1995) Uppaal\u2014a tool suite for automatic verification of real-time systems. In: Proc of workshop on verification and control of hybrid systems III. Oct 1995. LNCS, vol 1066. Springer, Berlin, pp 232\u2013243"},{"key":"46_CR4","series-title":"LNCS","volume-title":"Static analysis symposium, June 2000","author":"S Bensalem","year":"2000","unstructured":"Bensalem S, Bozga M, Fernandez J-C, Ghirvu L, Lakhnech Y (2000) A transformational approach for generating non-linear invariants. In: Static analysis symposium, June 2000. LNCS, vol 1824. Springer, Berlin"},{"key":"46_CR5","doi-asserted-by":"crossref","first-page":"751","DOI":"10.1016\/B978-044450813-3\/50014-X","volume-title":"Handbook of automated reasoning, vol\u00a0I","author":"A Bockmayr","year":"2001","unstructured":"Bockmayr A, Weispfenning V (2001) Solving numerical constraints. In: Robinson A, Voronkov A (eds) Handbook of automated reasoning, vol\u00a0I. Elsevier, Amsterdam, pp 751\u2013842. Chapter 12"},{"issue":"3","key":"46_CR6","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"GE Collins","year":"1991","unstructured":"Collins GE, Hong H (1991) Partial cylindrical algebraic decomposition for quantifier elimination. J Symb Comput 12(3):299\u2013328","journal-title":"J Symb Comput"},{"key":"46_CR7","series-title":"LNCS","volume-title":"11th static analysis symposium (SAS\u20192004)","author":"M Col\u00f3n","year":"2004","unstructured":"Col\u00f3n M (2004) Approximating the algebraic relational semantics of imperative programs. In: 11th static analysis symposium (SAS\u20192004). LNCS, vol 3148. Springer, Berlin"},{"key":"46_CR8","series-title":"LNCS","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 (2003) Linear invariant generation using non-linear constraint solving. In: Somenzi F, Hunt W Jr (eds) Computer aided verification. LNCS, vol 2725. Springer, Berlin, pp 420\u2013433"},{"key":"46_CR9","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM principles of programming languages, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"46_CR10","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among the variables of a program. In: ACM principles of programming languages, Jan 1978, pp 84\u201397","DOI":"10.1145\/512760.512770"},{"key":"46_CR11","volume-title":"Ideals, varieties and algorithms: an introduction to computational algebraic geometry and commutative algebra","author":"D Cox","year":"1991","unstructured":"Cox D, Little J, O\u2019Shea D (1991) Ideals, varieties and algorithms: an introduction to computational algebraic geometry and commutative algebra. Springer, Berlin"},{"key":"46_CR12","doi-asserted-by":"crossref","unstructured":"Forsman K (1991) Construction of Lyapunov functions using Gr\u00f6bner bases. In: Proc 30th IEEE CDC","DOI":"10.1109\/CDC.1991.261424"},{"key":"46_CR13","volume-title":"Computers and intractability: a guide to the theory of NP-completeness","author":"M Garey","year":"1999","unstructured":"Garey M, Johnson D (1999) Computers and intractability: a guide to the theory of NP-completeness. Freeman, New York"},{"issue":"2","key":"46_CR14","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N Halbwachs","year":"1997","unstructured":"Halbwachs N, Proy Y, Roumanoff P (1997) Verification of real-time systems using linear relation analysis. Formal Methods Syst Des 11(2):157\u2013185","journal-title":"Formal Methods Syst Des"},{"key":"46_CR15","first-page":"278","volume-title":"Logic in computer science, LICS 1996","author":"TA Henzinger","year":"1996","unstructured":"Henzinger TA (1996) The theory of hybrid automata. In: Logic in computer science, LICS 1996. IEEE Computer Society, Los Alamitos, pp 278\u2013292"},{"key":"46_CR16","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-60045-0_53","volume-title":"Computer-aided verification","author":"T Henzinger","year":"1995","unstructured":"Henzinger T, Ho P-H (1995) Algorithmic analysis of nonlinear hybrid systems. In: Computer-aided verification. LNCS, vol 939. Springer, Berlin, pp 225\u2013238"},{"key":"46_CR17","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid systems II","author":"TA Henzinger","year":"1995","unstructured":"Henzinger TA, Ho P (1995) HyTech: the Cornell hybrid technology tool. In: Hybrid systems II. LNCS, vol 999. Springer, Berlin, pp 265\u2013293"},{"key":"46_CR18","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M Karr","year":"1976","unstructured":"Karr M (1976) Affine relationships among variables of a program. Acta Inf 6:133\u2013151","journal-title":"Acta Inf"},{"key":"46_CR19","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G Lafferriere","year":"2001","unstructured":"Lafferriere G, Pappas G, Yovine S (2001) Symbolic reachability computation for families of linear vector fields. J Symb Comput 32:231\u2013253","journal-title":"J Symb Comput"},{"key":"46_CR20","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 (1995) Temporal verification of reactive systems: safety. Springer, New York"},{"key":"46_CR21","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/0020-0255(89)90037-6","volume":"48","author":"B Mishra","year":"1989","unstructured":"Mishra B, Yap C (1989) Notes on Gr\u00f6bner bases. Inf Sci 48:219\u2013252","journal-title":"Inf Sci"},{"key":"46_CR22","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/3-540-45789-5_4","volume-title":"Static analysis symposium (SAS 2002)","author":"M M\u00fcller-Olm","year":"2002","unstructured":"M\u00fcller-Olm M, Seidl H (2002) Polynomial constants are decidable. In: Static analysis symposium (SAS 2002). LNCS, vol 2477. Springer, Berlin, pp 4\u201319"},{"issue":"4","key":"46_CR23","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4):541\u2013580","journal-title":"Proc IEEE"},{"issue":"2","key":"46_CR24","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"PA Parillo","year":"2003","unstructured":"Parillo PA (2003) Semidefinite programming relaxation for semialgebraic problems. Math Program Ser B 96(2):293\u2013320","journal-title":"Math Program Ser B"},{"key":"46_CR25","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid systems: computation and control","author":"S Prajna","year":"2004","unstructured":"Prajna S, Jadbabaie A (2004) Safety verification using barrier certificates. In: Hybrid systems: computation and control. LNCS, vol 2993. Springer, Berlin, pp 477\u2013492"},{"key":"46_CR26","series-title":"LNCS","volume-title":"11th static analysis symposium (SAS\u20192004)","author":"E Rodriguez-Carbonell","year":"2004","unstructured":"Rodriguez-Carbonell E, Kapur D (2004) An abstract interpretation approach for automatic generation of polynomial invariants. In: 11th static analysis symposium (SAS\u20192004). LNCS, vol 3148. Springer, Berlin"},{"key":"46_CR27","doi-asserted-by":"crossref","unstructured":"Rodriguez-Carbonell E, Kapur D (2004) Automatic generation of polynomial loop invariants: algebraic foundations. In: Proc international symp on symbolic and algebraic computation, ISSAC-2004, Spain","DOI":"10.1145\/1005285.1005324"},{"key":"46_CR28","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"682","DOI":"10.1007\/978-3-540-39910-0_29","volume-title":"Verification: theory and practice","author":"S Sankaranarayanan","year":"2003","unstructured":"Sankaranarayanan S, Sipma HB, Manna Z (2003) Petri net analysis using invariant generation. In: Verification: theory and practice. LNCS, vol 2772. Springer, Berlin, pp 682\u2013701"},{"key":"46_CR29","first-page":"318","volume-title":"ACM principles of programming languages (POPL)","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan S, Sipma H, Manna Z (2004) Non-linear loop invariant generation using Gr\u00f6bner bases. In: ACM principles of programming languages (POPL). ACM, New York, pp 318\u2013330"},{"key":"46_CR30","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"11th static analysis symposium (SAS\u20192004)","author":"S Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan S, Sipma HB, Manna Z (2004) Constraint-based linear relations analysis. In: 11th static analysis symposium (SAS\u20192004). LNCS, vol 3148. Springer, Berlin, pp 53\u201368"},{"key":"46_CR31","unstructured":"Silva B, Richeson K, Krogh B, Chutinan A (2000) Modeling and verifying hybrid dynamic systems using CheckMate. In: Proc conf on automation of mixed processes: hybrid dynamic systems, pp 323\u2013328"},{"key":"46_CR32","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1007\/3-540-36580-X_37","volume-title":"Hybrid systems: computation and control HSCC","author":"A Tiwari","year":"2003","unstructured":"Tiwari A (2003) Approximate reachability for linear systems. In: Hybrid systems: computation and control HSCC. LNCS, vol 2623. Springer, Berlin, pp 514\u2013525"},{"key":"46_CR33","series-title":"LNCS","first-page":"477","volume-title":"Hybrid systems: computation and control","author":"A Tiwari","year":"2004","unstructured":"Tiwari A, Khanna G (2004) Non-linear systems: approximating reach sets. In: Hybrid systems: computation and control. LNCS, vol 2993. Springer, Berlin, pp 477\u2013492"},{"key":"46_CR34","series-title":"LNCS","first-page":"113","volume-title":"TACAS 2001","author":"A Tiwari","year":"2001","unstructured":"Tiwari A, Rue\u00df H, Sa\u00efdi H, Shankar N (2001) A technique for invariant generation. In: TACAS 2001. LNCS, vol 2031. Springer, Berlin, pp 113\u2013127"},{"key":"46_CR35","unstructured":"Windsteiger W, Buchberger B (1993) Gr\u00f6bner: a library for computing Gr\u00f6bner bases based on SACLIB. Tech rep, RISC-Linz"},{"key":"46_CR36","doi-asserted-by":"crossref","unstructured":"Yovine S (1997) Kronos: a verification tool for real-time systems. Springer International J Softw Tools Technol Transf 1, 1\/2, October 1997","DOI":"10.1007\/s100090050009"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-007-0046-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-007-0046-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-007-0046-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:01:03Z","timestamp":1559253663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-007-0046-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12,5]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,2]]}},"alternative-id":["46"],"URL":"https:\/\/doi.org\/10.1007\/s10703-007-0046-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12,5]]}}}