{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:40:41Z","timestamp":1780116041300,"version":"3.54.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642246890","type":"print"},{"value":"9783642246906","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24690-6_13","type":"book-chapter","created":{"date-parts":[[2011,10,25]],"date-time":"2011-10-25T01:35:37Z","timestamp":1319506537000},"page":"172-187","source":"Crossref","is-referenced-by-count":19,"title":["Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Eggers","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nacim","family":"Ramdani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nedialko","family":"Nedialkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Berz, M.: COSY INFINITY version 8 reference manual. Tech. Rep. MSUCL\u20131088, National Superconducting Cyclotron Lab., Michigan State University, USA (1997)"},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Commun. ACM\u00a05, 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"13_CR3","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-88387-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A. Eggers","year":"2008","unstructured":"Eggers, A., Fr\u00e4nzle, M., Herde, C.: SAT modulo ODE: A direct SAT approach to hybrid systems. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 171\u2013185. Springer, Heidelberg (2008)"},{"issue":"3-4","key":"13_CR5","first-page":"209","volume":"1","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT Special Issue on Constraint Programming and SAT\u00a01(3-4), 209\u2013236 (2007)","journal-title":"JSAT Special Issue on Constraint Programming and SAT"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-642-15396-9_20","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2010","author":"A. Goldsztejn","year":"2010","unstructured":"Goldsztejn, A., Mullier, O., Eveillard, D., Hosobe, H.: Including ordinary differential equations based constraints in the standard CP framework. In: Cohen, D. (ed.) CP 2010. LNCS, vol.\u00a06308, pp. 221\u2013235. Springer, Heidelberg (2010)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/3-540-46430-1_14","volume-title":"Hybrid Systems: Computation and Control","author":"T. Henzinger","year":"2000","unstructured":"Henzinger, T., Horowitz, B., Majumdar, R., Wong-Toi, H.: Beyond HYTECH: Hybrid systems analysis using interval numerical methods. In: Lynch, N., Krogh, B. (eds.) HSCC 2000. LNCS, vol.\u00a01790, pp. 130\u2013144. Springer, Heidelberg (2000)"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Ishii, D., Ueda, K., Hosobe, H.: An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems. International Journal on Software Tools for Technology Transfer (STTT), 1\u201313 (March 2011)","DOI":"10.1007\/s10009-011-0193-y"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Ishii, D., Ueda, K., Hosobe, H., Goldsztejn, A.: Interval-based solving of hybrid constraint systems. In: Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems, pp. 144\u2013149 (2009)","DOI":"10.3182\/20090916-3-ES-3003.00026"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Kieffer, M., Walter, E., Simeonov, I.: Guaranteed nonlinear parameter estimation for continuous-time dynamical models. In: Proceedings 14th IFAC Symposium on System Identification, Newcastle, Aus, pp. 843\u2013848 (2006)","DOI":"10.3182\/20060329-3-AU-2901.00133"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1007\/BF01475477","volume":"26","author":"M. M\u00fcller","year":"1927","unstructured":"M\u00fcller, M.: \u00dcber das Fundamentaltheorem in der Theorie der gew\u00f6hnlichen Differentialgleichungen. Mathematische Zeitschrift\u00a026, 619\u2013645 (1927)","journal-title":"Mathematische Zeitschrift"},{"key":"13_CR12","unstructured":"Nedialkov, N.S.: VNODE-LP \u2014 a validated solver for initial value problems in ordinary differential equations. Tech. Rep. CAS-06-06-NN, Department of Computing and Software, McMaster University, Hamilton, Ontario, L8S 4K1 (2006), VNODE-LP http:\/\/www.cas.mcmaster.ca\/~nedialk\/vnodelp"},{"key":"13_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-15956-5_1","volume-title":"Modeling, Design, and Simulation of Systems with Uncertainties, Mathematical Engineering","author":"N.S. Nedialkov","year":"2011","unstructured":"Nedialkov, N.S.: Implementing a rigorous ODE solver through literate programming. In: Rauh, A., Auer, E. (eds.) Modeling, Design, and Simulation of Systems with Uncertainties, Mathematical Engineering, vol.\u00a03, pp. 3\u201319. Springer, Heidelberg (2011)"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Nedialkov, N.S.: Computing Rigorous Bounds on the Solution of an Initial Value Problem for an Ordinary Differential Equation. Ph.D. thesis, Department of Computer Science, University of Toronto, Toronto, Canada, M5S 3G4 (February 1999)","DOI":"10.1007\/978-94-017-1247-7_23"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-540-75454-1_23","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Wagner, S.: Region stability proofs for hybrid systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol.\u00a04763, pp. 320\u2013335. Springer, Heidelberg (2007)"},{"issue":"10","key":"13_CR16","doi-asserted-by":"publisher","first-page":"2352","DOI":"10.1109\/TAC.2009.2028974","volume":"54","author":"N. Ramdani","year":"2009","unstructured":"Ramdani, N., Meslem, N., Candau, Y.: A hybrid bounding method for computing an over-approximation for the reachable space of uncertain nonlinear systems. IEEE Transactions on Automatic Control\u00a054(10), 2352\u20132364 (2009)","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"2","key":"13_CR17","first-page":"263","volume":"4","author":"N. Ramdani","year":"2010","unstructured":"Ramdani, N., Meslem, N., Candau, Y.: Computing reachable sets for uncertain nonlinear monotone systems. Nonlinear Analysis: Hybrid Systems\u00a04(2), 263\u2013278 (2010)","journal-title":"Nonlinear Analysis: Hybrid Systems"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Transactions in Embedded Computing Systems\u00a06(1) (2007)","DOI":"10.1145\/1210268.1210276"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/10722167_36","volume-title":"Computer Aided Verification","author":"O. Shtrichman","year":"2000","unstructured":"Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E., Sistla, A. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 480\u2013494. Springer, Heidelberg (2000)"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0031569","volume-title":"Hybrid Systems IV","author":"O. Stursberg","year":"1997","unstructured":"Stursberg, O., Kowalewski, S., Hoffmann, I., Preu\u00dfig, J.: Comparing timed and hybrid automata as approximations of continuous systems. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1996. LNCS, vol.\u00a01273, pp. 361\u2013377. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24690-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,18]],"date-time":"2019-06-18T14:33:32Z","timestamp":1560868412000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24690-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642246890","9783642246906"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24690-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}