{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T11:48:33Z","timestamp":1743076113708,"version":"3.40.3"},"publisher-location":"Wiesbaden","reference-count":18,"publisher":"Springer Fachmedien Wiesbaden","isbn-type":[{"type":"print","value":"9783658099930"},{"type":"electronic","value":"9783658099947"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-658-09994-7_16","type":"book-chapter","created":{"date-parts":[[2015,6,5]],"date-time":"2015-06-05T07:56:17Z","timestamp":1433490977000},"page":"290-292","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An SMT-based Approach to analyze Non-Linear Relations of Parameters for Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Xian","family":"Li","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,6,6]]},"reference":[{"key":"16_CR1","first-page":"41","volume-title":"Hybrid Systems: Computation and Control (HSCC)","author":"K. Bauer","year":"2010","unstructured":"Bauer, K., Schneider, K.: From synchronous programs to symbolic representations of hybrid systems. In Johansson, K., Yi, W., eds.: Hybrid Systems: Computation and Control (HSCC), Stockholm, Sweden, ACM (2010) 41\u201350"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: HyDI: A language for symbolic hybrid systems with discrete interaction. In: Software Engineering and Advanced Applications (SEAA), 2011 37th EUROMICRO Conference on, IEEE Computer Society (2011) 275\u2013278","DOI":"10.1109\/SEAA.2011.49"},{"key":"16_CR3","unstructured":"Li, X., Schneider, K.: A counterexample-guided approach to symbolic simulation of hybrid systems. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), Chemnitz, Germany, In proceeding (2015)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional satisfiability and constraint programming: A comparative survey. ACM Computing Surveys (CSUR) 38 (2006)","DOI":"10.1145\/1177352.1177354"},{"key":"16_CR5","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M. Franzle","year":"2007","unstructured":"Franzle, M., Herde, C.: HySAT: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design (FMSD) 30 (2007) 179\u2013198","journal-title":"Formal Methods in System Design"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Joost Schaafsma, B., Sebastiani, R.: The MathSAT5 SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Volume\u00a07795 of LNCS., Rome, Italy, Springer (2013) 93\u2013107","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"16_CR7","unstructured":"CVC4. cvc4.cs.nyu.edu\/web\/"},{"key":"16_CR8","unstructured":"Z3. z3.codeplex.com\/"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems \u2013 Proving Theorems for Complex Dynamics. Springer (2010)","DOI":"10.1007\/978-3-642-14509-4"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Andre, E., Fribourg, L., K\u00fchne, U., Soulat, R.: IMITATOR 2.5: A tool for analyzing robustness in scheduling problems. In: Proceedings of the 18th International Symposium on Formal Methods (FM\u201912). Volume\u00a07436 of Lecture Notes in Computer Science., Paris, France, Springer (2012) 33\u201336","DOI":"10.1007\/978-3-642-32759-9_6"},{"key":"16_CR11","first-page":"379","volume-title":"SpaceEx: Scalable verification of hybrid systems. In: Computer Aided Verification (CAV). Volume\u00a06806 of LNCS., Snowbird, Utah","author":"G. Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donze, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable verification of hybrid systems. In: Computer Aided Verification (CAV). Volume\u00a06806 of LNCS., Snowbird, Utah, USA, Springer (2011) 379\u2013395"},{"key":"16_CR12","first-page":"368","volume-title":"TReX: A tool for reachability analysis of complex systems. In: Computer Aided Verification (CAV). Volume\u00a02102 of LNCS","author":"A. Annichini","year":"2001","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: A tool for reachability analysis of complex systems. In: Computer Aided Verification (CAV). Volume\u00a02102 of LNCS., Paris, France, Springer (2001) 368\u2013372"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Eggers, A., Franzle, M., Herde, C.: SAT modulo ODE: A direct SAT approach to hybrid systems. In: Automated Technology for Verification and Analysis (ATVA). Volume\u00a05311 of LNCS., Seoul, South Korea, Springer (2008) 171\u2013185","DOI":"10.1007\/978-3-540-88387-6_14"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.: dReal: An SMT solver for nonlinear theories over the reals. In: Conference on Automated Deduction (CADE). Volume\u00a07898 of LNCS., Lake Placid, NY, USA, Springer (2013) 208\u2013214","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"16_CR15","unstructured":"QEPCAD. http:\/\/www.usna.edu\/CS\/qepcadweb\/B\/QEPCAD.html"},{"key":"16_CR16","unstructured":"Reduce. reduce-algebra.com\/"},{"key":"16_CR17","first-page":"186","volume":"5","author":"P. Bonami","year":"2008","unstructured":"Bonami, P., Biegler, L., Conn, A., CornueJols, G., Grossmann, I., Laird, C., Lee, J., Lodi, A., Margot, F., Sawaya, N., W\u00fcchter, A.: An algorithmic framework for convex mixed integer nonlinear programs. Discret. Optim. 5 (2008) 186\u2013204","journal-title":"Optim"},{"key":"16_CR18","unstructured":"Schneider, K.: The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany (2009)"}],"container-title":["Formal Modeling and Verification of Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-658-09994-7_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T17:08:01Z","timestamp":1675271281000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-658-09994-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783658099930","9783658099947"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-658-09994-7_16","relation":{},"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"6 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}