{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T03:36:19Z","timestamp":1770435379847,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540883869","type":"print"},{"value":"9783540883876","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-88387-6_14","type":"book-chapter","created":{"date-parts":[[2008,10,10]],"date-time":"2008-10-10T01:42:45Z","timestamp":1223602965000},"page":"171-185","source":"Crossref","is-referenced-by-count":34,"title":["SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Eggers","sequence":"first","affiliation":[]},{"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Herde","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"HSCC 2004","year":"2004","unstructured":"Alur, R., Pappas, G.J. (eds.): HSCC 2004. LNCS, vol.\u00a02993. Springer, Heidelberg (2004)"},{"key":"14_CR2","unstructured":"Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying industrial hybrid systems with MathSAT. ENTCS\u00a089(4) (2004)"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1016\/S1574-6526(06)80020-9","volume-title":"Handbook of Constraint Programming, Foundations of Artificial Intelligence","author":"F. Benhamou","year":"2006","unstructured":"Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, Foundations of Artificial Intelligence, ch.\u00a016, pp. 571\u2013603. Elsevier, Amsterdam (2006)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579. Springer, Heidelberg (1999)"},{"key":"14_CR5","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. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"14_CR6","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)"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Fehnker, A., Ivan\u010di\u0107, F.: Benchmarks for hybrid systems verification. In: Alur, Pappas (eds.) in [1] pp. 326\u2013341","DOI":"10.1007\/978-3-540-24743-2_22"},{"issue":"3","key":"14_CR8","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C.: HySAT: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in Syst. Design\u00a030(3), 179\u2013198 (2007)","journal-title":"Formal Methods in Syst. Design"},{"key":"14_CR9","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, 209\u2013236 (2007)","journal-title":"JSAT Special Issue on Constraint Programming and SAT"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(t): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114. Springer, Heidelberg (2004)"},{"key":"14_CR11","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.A. Henzinger","year":"2000","unstructured":"Henzinger, T.A., Horowitz, B., Majumdar, R., Wong-Toi, H.: Beyond HYTECH: Hybrid systems analysis using interval numerical methods. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, pp. 130\u2013144. Springer, Heidelberg (2000)"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Hickey, T., Wittenberg, D.: Rigorous modeling of hybrid systems using interval arithmetic constraints. In: Alur, Pappas (eds.) in [1], pp. 402\u2013416","DOI":"10.1007\/978-3-540-24743-2_27"},{"key":"14_CR13","first-page":"255","volume-title":"Computerarithmetic: Scientific Computation and Programming Languages","author":"R.J. Lohner","year":"1987","unstructured":"Lohner, R.J.: Enclosing the solutions of ordinary initial and boundary value problems. In: Computerarithmetic: Scientific Computation and Programming Languages, pp. 255\u2013286. Teubner, Stuttgart (1987)"},{"key":"14_CR14","first-page":"103","volume-title":"Error in Digital Computation","author":"R.E. Moore","year":"1965","unstructured":"Moore, R.E.: Automatic local coordinate transformation to reduce the growth of error bounds in interval computation of solutions of ordinary differential equations. In: Ball, L.B. (ed.) Error in Digital Computation, vol.\u00a0II, pp. 103\u2013140. Wiley, New York (1965)"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-540-78929-1_30","volume-title":"Hybrid Systems: Computation and Control","author":"N. Ramdani","year":"2008","unstructured":"Ramdani, N., Meslem, N., Candau, Y.: Rechability of unvertain nonlinear systems using a nonlinear hybridization. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol.\u00a04981, pp. 415\u2013428. Springer, Heidelberg (2008)"},{"key":"14_CR16","unstructured":"Stauning, O.: Automatic Validation of Numerical Solutions. PhD thesis, Danmarks Tekniske Universitet, Kgs.Lyngby, Denmark (1997)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88387-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T10:45:38Z","timestamp":1557830738000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88387-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540883869","9783540883876"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88387-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}