{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T19:54:01Z","timestamp":1791316441266,"version":"4.3.1"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705437","type":"print"},{"value":"9783540705451","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70545-1_18","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"190-203","source":"Crossref","is-referenced-by-count":81,"title":["Constraint-Based Approach for Analysis of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Sumit","family":"Gulwani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"3","key":"18_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138(3), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"18_CR2","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R. Alur","year":"2000","unstructured":"Alur, R., Henzinger, T., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proceedings of the IEEE\u00a088(2), 971\u2013984 (2000)","journal-title":"Proceedings of the IEEE"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0004-3702(01)00169-2","volume":"136","author":"O. Bernard","year":"2002","unstructured":"Bernard, O., Gouze, J.-L.: Global qualitative description of a class of nonlinear dynamical systems. Artificial Intelligence\u00a0136, 29\u201359 (2002)","journal-title":"Artificial Intelligence"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T., Majumdar, R., Rybalchenko, A.: Invariant Synthesis for Combined Theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 378\u2013394. Springer, Heidelberg (2007)"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"1747","DOI":"10.1016\/S0005-1098(99)00113-2","volume":"35","author":"F. Blanchini","year":"1999","unstructured":"Blanchini, F.: Set invariance in control. Automatica\u00a035, 1747\u20131767 (1999)","journal-title":"Automatica"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48983-5_10","volume-title":"Hybrid Systems: Computation and Control","author":"A. Chutinan","year":"1999","unstructured":"Chutinan, A., Krogh, B.H.: Verification of Polyhedral-Invariant Hybrid Automata Using Polygonal Flow Pipe Approximations. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol.\u00a01569. Springer, Heidelberg (1999)"},{"key":"18_CR7","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.: 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":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for dpll(t). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006), http:\/\/yices.csl.sri.com\/"},{"issue":"4","key":"18_CR9","doi-asserted-by":"publisher","first-page":"1125","DOI":"10.1109\/25.330177","volume":"43","author":"D. Godbole","year":"1994","unstructured":"Godbole, D., Lygeros, J.: Longitudinal control of the lead car of a platoon. IEEE Transactions on Vehicular Technology\u00a043(4), 1125\u20131135 (1994)","journal-title":"IEEE Transactions on Vehicular Technology"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proc. PLDI (2008)","DOI":"10.1145\/1375581.1375616"},{"key":"18_CR11","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer\u00a01, 110\u2013122 (1997)","journal-title":"Software Tools for Technology Transfer"},{"key":"18_CR12","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Deduction and Applications (2005)"},{"issue":"3","key":"18_CR13","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G. Lafferriere","year":"2001","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computations for families of linear vector fields. J. Symbolic Computation\u00a032(3), 231\u2013253 (2001)","journal-title":"J. Symbolic Computation"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Parker, R.S., Doyle, F.J., Peppas, N.A.: A model-based algorithm for blood glucose control in type I diabetes patients. IEEE Trans BioMed Eng.\u00a046(2) (1999)","DOI":"10.1109\/10.740877"},{"key":"18_CR15","unstructured":"Parrilo, P.A.: Structured semidefinite programs and semialgebraic geometric methods in robustness and optimization. PhD thesis, California Inst. of Tech. (2000)"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Prajna, S.: Barrier certificates for nonlinear model validation. In: Proc. IEEE Conference on Decision and Control (2003)","DOI":"10.1109\/CDC.2003.1273063"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","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.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 477\u2013492. Springer, Heidelberg (2004)"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Aut. Control (2005)","DOI":"10.1109\/CDC.2004.1428804"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Puri, A., Varaiya, P.: Driving safely in smart cars. In: Proceedings of the 1995 American Control Conference (1995)","DOI":"10.1109\/ACC.1995.533807"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1007\/978-3-540-31954-2_38","volume-title":"Hybrid Systems: Computation and Control","author":"E. Rodriguez-Carbonell","year":"2005","unstructured":"Rodriguez-Carbonell, E., Tiwari, A.: Generating polynomial invariants for hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 590\u2013605. Springer, Heidelberg (2005)"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using gr\u00f6bner bases. In: POPL 2004 (2004)","DOI":"10.1145\/964001.964028"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"539","DOI":"10.1007\/978-3-540-24743-2_36","volume-title":"Hybrid Systems: Computation and Control","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Constructing invariants for hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 539\u2013554. Springer, Heidelberg (2004)"},{"key":"18_CR23","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":"18_CR24","unstructured":"Sorensen, J.T.: A physiologic model of glucose metabolism in man and its use to design and assess improved insulin therapies for diabetes. PhD thesis, Dept. Chem. Eng., Massachusetts Inst. Technology (MIT), Cambridge (1985)"},{"issue":"10","key":"18_CR25","doi-asserted-by":"publisher","first-page":"1269","DOI":"10.1016\/j.conengprac.2004.04.002","volume":"12","author":"O. Stursberg","year":"2004","unstructured":"Stursberg, O., Fehnker, A., Han, Z., Krogh, B.H.: Verification of a cruise control system using counterexample-guided search. Control Engineering Practice\u00a012(10), 1269\u20131278 (2004)","journal-title":"Control Engineering Practice"},{"key":"18_CR26","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press (1948)"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/3-540-36580-X_37","volume-title":"Hybrid Systems: Computation and Control","author":"A. Tiwari","year":"2003","unstructured":"Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 514\u2013525. Springer, Heidelberg (2003)"},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Yazarel, H., Pappas, G.J.: Geometric programming relaxations for linear system reachability. In: Proc. 2004 American Control Conference (2004)","DOI":"10.23919\/ACC.2004.1383661"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Yazarel, H., Prajna, S., Pappas, G.J.: S.O.S. for safety. In: Proc. 43rd IEEE Conference on Decision and Control (2004)","DOI":"10.1109\/CDC.2004.1428673"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70545-1_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:07:37Z","timestamp":1605744457000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70545-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705437","9783540705451"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70545-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}