{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T21:42:25Z","timestamp":1762033345139,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319307336"},{"type":"electronic","value":"9783319307343"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30734-3_8","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:19:52Z","timestamp":1457770792000},"page":"88-103","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Compositional Approach to the Verification of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"L\u0103cr\u0103mioara","family":"A\u015ftef\u0103noaei","sequence":"first","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,13]]},"reference":[{"key":"8_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. Theor. Comput. Sci. 138, 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-54862-8_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L A\u015ftef\u0103noaei","year":"2014","unstructured":"A\u015ftef\u0103noaei, L., Rayana, S.B., Bensalem, S., Bozga, M., Combaz, J.: Compositional invariant generation for timed systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 263\u2013278. Springer, Heidelberg (2014)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/978-3-319-17524-9_6","volume-title":"NASA Formal Methods","author":"L A\u015ftef\u0103noaei","year":"2015","unstructured":"A\u015ftef\u0103noaei, L., Rayana, S.B., Bensalem, S., Bozga, M., Combaz, J.: Compositional verification of parameterised timed systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 66\u201381. Springer, Heidelberg (2015)"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: HSCC (2015)","DOI":"10.1145\/2728606.2728630"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-88387-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"S Bensalem","year":"2008","unstructured":"Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional verification for component-based systems and application. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 64\u201379. Springer, Heidelberg (2008)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-642-39176-7_8","volume-title":"Model Checking Software","author":"S Bogomolov","year":"2013","unstructured":"Bogomolov, S., Donz\u00e9, A., Frehse, G., Grosu, R., Johnson, T.T., Ladan, H., Podelski, A., Wehrle, M.: Abstraction-based guided search for hybrid systems. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 117\u2013134. Springer, Heidelberg (2013)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Larraz, D., Oliveras, A., Carbonell, E.R., Rubio, A.: Compositional safety verification with max-smt. In: FMCAD (2015)","DOI":"10.1109\/FMCAD.2015.7542250"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: An analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/978-3-319-17524-9_29","volume-title":"NASA Formal Methods","author":"X Chen","year":"2015","unstructured":"Chen, X., Schupp, S., Makhlouf, I.B., \u00c1brah\u00e1m, E., Frehse, G., Kowalewski, S.: A benchmark suite for hybrid systems reachability analysis. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 408\u2013414. Springer, Heidelberg (2015)"},{"key":"8_CR10","unstructured":"Cimatti, A.: Application of SMT solvers to hybrid system verification. In: FMCAD (2012)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Parameter synthesis with IC3. In: FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679406"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/978-3-662-46681-0_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: An SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52\u201367. Springer, Heidelberg (2015)"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/BF00709157","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Formal Methods Syst. Des. 1, 385\u2013415 (1992)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Damm, W., M\u00f6hlmann, E., Rakow, A.: Component based design of hybrid systems: a case study on concurrency and coupling. In: HSCC (2014)","DOI":"10.1145\/2562059.2562120"},{"key":"8_CR15","unstructured":"David, A., Larsen, K.G., Legay, A., Poulsen, D.B.: Statistical model checking of dynamic networks of stochastic hybrid automata. ECEASST 66 (2013)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, A toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167\u2013170. Springer, Heidelberg (2010)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-24690-6_13","volume-title":"Software Engineering and Formal Methods","author":"A Eggers","year":"2011","unstructured":"Eggers, A., Ramdani, N., Nedialkov, N., Fr\u00e4nzle, M.: Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 172\u2013187. Springer, Heidelberg (2011)"},{"key":"8_CR18","unstructured":"Frehse, G.: Compositional Verification of Hybrid Systems using Simulation Relations. Ph.D. thesis, Radboud Universiteit Nijmegen (2005)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-78929-1_14","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2008","unstructured":"Frehse, G., Jha, S.K., Krogh, B.H.: A counterexample-guided approach to parameter synthesis for linear hybrid automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 187\u2013200. Springer, Heidelberg (2008)"},{"key":"8_CR21","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1142\/S0129054113400091","volume":"24","author":"L Fribourg","year":"2013","unstructured":"Fribourg, L., K\u00fchne, U.: Parametric verification and test coverage for hybrid automata using the inverse method. Int. J. Found. Comput. Sci. 24, 233\u2013249 (2013)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-78499-9_33","volume-title":"Foundations of Software Science and Computational Structures","author":"P Habermehl","year":"2008","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 474\u2013489. Springer, Heidelberg (2008)"},{"key":"8_CR23","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: LICS (1996)"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-45351-2_24","volume-title":"Hybrid Systems: Computation and Control","author":"TA Henzinger","year":"2001","unstructured":"Henzinger, T.A., Minea, M., Prabhu, V.S.: Assume-guarantee reasoning for hierarchical hybrid systems. In: Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 275\u2013290. Springer, Heidelberg (2001)"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027241","volume-title":"Formal Methods for Industrial Applications","author":"TA Henzinger","year":"1996","unstructured":"Henzinger, T.A., Wong-Toi, H.: Using HyTech to synthesize control parameters for a steam boiler. In: Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.) FMIA 1996. LNCS, vol. 1165. Springer, Heidelberg (1996)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-40184-8_26","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"H Hermanns","year":"2013","unstructured":"Hermanns, H., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J.: Compositional verification and optimization of interactive markov chains. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 \u2013 Concurrency Theory. LNCS, vol. 8052, pp. 364\u2013379. Springer, Heidelberg (2013)"},{"key":"8_CR27","unstructured":"Ho, P.-H.: Automatic Analysis of Hybrid Systems. Ph.D. thesis, Cornell University (1995)"},{"key":"8_CR28","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/32.75414","volume":"17","author":"MS Jaffe","year":"1991","unstructured":"Jaffe, M.S., Leveson, N.G., Heimdahl, M.P.E., Melhart, B.E.: Software requirements analysis for real-time process-control systems. IEEE Trans. Softw. Eng. 17, 241\u2013258 (1991)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Jeannin, J., Platzer, A.: dtl2: Differential temporal dynamic logic with nested temporalities for hybrid systems. In: IJCAR (2014)","DOI":"10.1007\/978-3-319-08587-6_22"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-30793-5_2","volume-title":"Formal Techniques for Distributed Systems","author":"TT Johnson","year":"2012","unstructured":"Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Giese, H., Rosu, G. (eds.) FORTE 2012 and FMOODS 2012. LNCS, vol. 7273, pp. 18\u201334. Springer, Heidelberg (2012)"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/978-3-319-10512-3_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"TT Johnson","year":"2014","unstructured":"Johnson, T.T., Mitra, S.: Anonymized reachability of hybrid automata networks. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 130\u2013145. Springer, Heidelberg (2014)"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-662-46681-0_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kong","year":"2015","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.: $${\\sf dReach}$$: $$\\delta $$-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200\u2013205. Springer, Heidelberg (2015)"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Legay, A., Bensalem, S., Boyer, B., Bozga, M.: Incremental generation of linear invariants for component-based systems. In: ACSD (2013)","DOI":"10.1109\/ACSD.2013.11"},{"key":"8_CR34","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"NA Lynch","year":"2003","unstructured":"Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid I\/O automata. Inf. Comput. 185, 105\u2013157 (2003)","journal-title":"Inf. Comput."},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L de Moura","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"8_CR36","unstructured":"Mover, S.: Verification of Hybrid Systems using Satisfiability Modulo Theories. Ph.D. thesis, FBK-IRST\/DIT (2014)"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Mover, S., Cimatti, A., Tiwari, A., Tonetta, S.: Time-aware relational abstractions for hybrid systems. In: EMSOFT (2013)","DOI":"10.1109\/EMSOFT.2013.6658592"},{"key":"8_CR38","unstructured":"Oehlerking, J.: Decomposition of Stability Proofs for Hybrid Systems. Ph.D. thesis, Carl von Ossietzky Universit\u00e4t, Oldenburg (2011)"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-642-31365-3_34","volume-title":"Automated Reasoning","author":"J-D Quesel","year":"2012","unstructured":"Quesel, J.-D., Platzer, A.: Playing hybrid games with KeYmaera. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 439\u2013453. Springer, Heidelberg (2012)"},{"key":"8_CR40","unstructured":"Somenzi, F., Bradley, A.R.: IC3: where monolithic and incremental meet. In: FMCAD (2011)"},{"key":"8_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-319-02444-8_37","volume-title":"Automated Technology for Verification and Analysis","author":"R Testylier","year":"2013","unstructured":"Testylier, R., Dang, T.: NLTOOLBOX: A library for reachability computation of nonlinear dynamical systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 469\u2013473. Springer, Heidelberg (2013)"},{"key":"8_CR42","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1016\/S0947-3580(12)71160-3","volume":"18","author":"L Zhang","year":"2012","unstructured":"Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M.: Safety verification for probabilistic hybrid systems. Eur. J. Control 18, 588\u2013590 (2012)","journal-title":"Eur. J. Control"}],"container-title":["Lecture Notes in Computer Science","Theory and Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30734-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T12:25:49Z","timestamp":1720787149000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-30734-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319307336","9783319307343"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30734-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}