{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:21:59Z","timestamp":1778498519356,"version":"3.51.4"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,11,16]],"date-time":"2012-11-16T00:00:00Z","timestamp":1353024000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10270-012-0295-3","type":"journal-article","created":{"date-parts":[[2012,11,15]],"date-time":"2012-11-15T16:29:29Z","timestamp":1352996969000},"page":"121-148","source":"Crossref","is-referenced-by-count":32,"title":["Improving the SAT modulo ODE approach to hybrid systems analysis by combining different enclosure methods"],"prefix":"10.1007","volume":"14","author":[{"given":"Andreas","family":"Eggers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nacim","family":"Ramdani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nedialko S.","family":"Nedialkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,11,16]]},"reference":[{"key":"295_CR1","unstructured":"Berz, M.: COSY INFINITY version 8 reference manual. Tech. Rep. MSUCL-1088, National Superconducting Cyclotron Laboratory, Michigan State University, USA (1997)"},{"key":"295_CR2","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Stursberg, O., Theobald, M.: Verification of hybrid systems based on counterexample-guided abstraction refinement. In: Gravel, H., Hatcliff, J. (eds.) TACAS, Lecture Notes in Computer Science vol 2619, pp. 192\u2013207. Springer, Berlin (2003)","DOI":"10.1007\/3-540-36577-X_14"},{"issue":"3","key":"295_CR3","doi-asserted-by":"crossref","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. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"295_CR4","doi-asserted-by":"crossref","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 5, 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"295_CR5","doi-asserted-by":"crossref","unstructured":"Eggers, A., Fr\u00e4nzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: ATVA, LNCS, vol. 5311, pp. 171\u2013185. Springer, New York (2008)","DOI":"10.1007\/978-3-540-88387-6_14"},{"key":"295_CR6","unstructured":"Eggers, A., Ramdani, N., Nedialkov, NS., Fr\u00e4nzle, M.: Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods. In: Barthe, G., Pardo, A., Schneider, G. (eds.) Proceedings of the Ninth International Conference on Software Engineering and Formal Methods (SEFM), LNCS, vol. 7041, pp. 172\u2013187. Springer, Berlin (2011). doi: 10.1007\/978-3-642-24690-6-13"},{"key":"295_CR7","doi-asserted-by":"crossref","unstructured":"Fousse, L., Hanrot, G., Lef\u00e8vre, V., P\u00e9lissier, P., Zimmermann, P.: MPFR: a multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33(2) (2007). doi: 10.1145\/1236463.1236468 , MPFR is available at http:\/\/www.mpfr.org\/","DOI":"10.1145\/1236463.1236468"},{"issue":"3\u20134","key":"295_CR8","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 1(3\u20134), 209\u2013236 (2007)","journal-title":"JSAT"},{"key":"295_CR9","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/978-3-642-15396-9_20","volume-title":"Principles and Practice of Constraint Programming\u2014CP 2010, LNCS, vol. 6308","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.) Principles and Practice of Constraint Programming\u2014CP 2010, LNCS, vol. 6308, pp. 221\u2013235. Springer, Berlin (2010)"},{"key":"295_CR10","doi-asserted-by":"crossref","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.) Hybrid Systems: Computation and Control, LNCS, vol. 1790, pp. 130\u2013144. Springer, New York (2000)","DOI":"10.1007\/3-540-46430-1_14"},{"key":"295_CR11","doi-asserted-by":"crossref","unstructured":"Ishii, D., Ueda, K., Hosobe, H.: An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems. Int. J. Softw. Tools Technol. Transf. (STTT), 1\u201313 (2011). doi: 10.1007\/s10009-011-0193-y","DOI":"10.1007\/s10009-011-0193-y"},{"key":"295_CR12","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, pp. 843\u2013848 (2006)","DOI":"10.3182\/20060329-3-AU-2901.00133"},{"key":"295_CR13","doi-asserted-by":"crossref","unstructured":"Lerch, M., Tischler, G., Gudenberg, J.W.V., Hofschuster, W., Kr\u00e4mer, W. Filib++, a fast interval library supporting containment computations. ACM Trans. Math. Softw. 32(2):299\u2013324 (2006). doi: 10.1145\/1141885.1141893 , FILIB++ is available at http:\/\/www2.math.uni-wuppertal.de\/~xsc\/software\/filib.html","DOI":"10.1145\/1141885.1141893"},{"key":"295_CR14","doi-asserted-by":"crossref","unstructured":"Lygeros, J., Johansson, K., Simic, S., Zhang, J., Sastry, S.: Dynamical properties of hybrid automata. IEEE Trans. Autom. Control 48(1), 2\u201317 (2003). doi: 10.1109\/TAC.2002.806650","DOI":"10.1109\/TAC.2002.806650"},{"key":"295_CR15","doi-asserted-by":"crossref","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 26, 619\u2013645 (1927)","journal-title":"Mathematische Zeitschrift"},{"key":"295_CR16","doi-asserted-by":"crossref","unstructured":"Nedialkov, N.S.: Computing rigorous bounds on the solution of an initial value problem for an ordinary differential equation. PhD thesis, Department of Computer Science, University of Toronto, Toronto, M5S 3G4 (1999)","DOI":"10.1007\/978-94-017-1247-7_23"},{"key":"295_CR17","unstructured":"Nedialkov, N.S.: VNODE-LP\u2014a validated solver for initial value problems in ordinary differential equations. Tech. Rep. CAS-06-06-NN. Department of Computing and Software, McMaster University, Hamilton, L8S 4K1, VNODE-LP is available at http:\/\/www.cas.mcmaster.ca\/~nedialk\/vnodelp (2006)"},{"key":"295_CR18","doi-asserted-by":"crossref","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. 3, pp. 3\u201319. Springer, New York (2011). doi: 10.1007\/978-3-642-15956-5_1","DOI":"10.1007\/978-3-642-15956-5_1"},{"key":"295_CR19","first-page":"320","volume-title":"FORMATS, LNCS, vol. 4763","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, LNCS, vol. 4763, pp. 320\u2013335. Springer, Berlin (2007)"},{"issue":"10","key":"295_CR20","doi-asserted-by":"crossref","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 Trans. Autom. Control 54(10), 2352\u20132364 (2009)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"2","key":"295_CR21","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/j.nahs.2009.10.002","volume":"4","author":"N Ramdani","year":"2010","unstructured":"Ramdani, N., Meslem, N., Candau, Y.: Computing reachable sets for uncertain nonlinear monotone systems. Nonlinear Anal. Hybrid Syst. 4(2), 263\u2013278 (2010)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"295_CR22","doi-asserted-by":"crossref","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans. Embed. Comput. Syst. 6(1), (2007)","DOI":"10.1145\/1210268.1210276"},{"key":"295_CR23","doi-asserted-by":"crossref","unstructured":"Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E., Sistla, A. (eds.) Computer Aided Verification, LNCS, vol. 1855, pp. 480\u2013494. Springer, Berlin (2000). doi: 10.1007\/10722167_36","DOI":"10.1007\/10722167_36"},{"key":"295_CR24","unstructured":"Stauning, O.: Automatic validation of numerical solutions. PhD thesis, Technical University of Denmark, Lyngby, (1997). http:\/\/www2.imm.dtu.dk\/documents\/ftp\/phdliste\/phd36_97.ps , FADBAD++ is available at http:\/\/www.fadbad.com"},{"key":"295_CR25","doi-asserted-by":"crossref","unstructured":"Stursberg, O., Kowalewski, S., Hoffmann, I., Preu\u00dfig, J.: Comparing timed and hybrid automata as approximations of continuous systems. In: Antsakalis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) Hybrid Systems IV, LNCS, vol. 1273, pp. 361\u2013377. Springer, Berlin (1997). doi: 10.1007\/bfb0031569","DOI":"10.1007\/BFb0031569"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-012-0295-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-012-0295-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-012-0295-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,31]],"date-time":"2022-01-31T10:39:01Z","timestamp":1643625541000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-012-0295-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,16]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["295"],"URL":"https:\/\/doi.org\/10.1007\/s10270-012-0295-3","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,11,16]]}}}