{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:24:25Z","timestamp":1742912665696,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319489889"},{"type":"electronic","value":"9783319489896"}],"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-48989-6_4","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T01:31:19Z","timestamp":1478482279000},"page":"60-68","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Compositional Parameter Synthesis"],"prefix":"10.1007","author":[{"given":"Lacramioara","family":"A\u015ftef\u0103noaei","sequence":"first","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[]},{"given":"Chih-Hong","family":"Cheng","sequence":"additional","affiliation":[]},{"given":"Harald","family":"Ruess","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: ACM, pp. 592\u2013601 (1993)","key":"4_CR1","DOI":"10.1145\/167088.167242"},{"doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9.: IMITATOR II: a tool for solving the good parameters problem in timed automata. In: INFINITY (2010)","key":"4_CR2","DOI":"10.4204\/EPTCS.39.7"},{"doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9., Soulat, R.: Synthesis of timing parameters satisfying safety properties. In: Reachability Problems (2011)","key":"4_CR3","DOI":"10.1007\/978-3-642-24288-5_5"},{"key":"4_CR4","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., Bensalem, S., Bozga, M., Combaz, J.: Compositional invariant generation for timed systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 263\u2013278. Springer, Heidelberg (2014). doi:\n                      10.1007\/978-3-642-54862-8_18"},{"key":"4_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). doi:\n                      10.1007\/978-3-540-88387-6_7"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: \n                      \n                        \n                      \n                      $${\\nu }$$\n                    Z - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). doi:\n                      10.1007\/978-3-662-46681-0_14"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-28891-3_28","volume-title":"NASA Formal Methods","author":"R Bruttomesso","year":"2012","unstructured":"Bruttomesso, R., Carioni, A., Ghilardi, S., Ranise, S.: Automated analysis of parametric timing-based mutual exclusion algorithms. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 279\u2013294. Springer, Heidelberg (2012). doi:\n                      10.1007\/978-3-642-28891-3_28"},{"unstructured":"Cheng, C., Guelfirat, T., Messinger, C., Schmitt, J.O., Schnelte, M., Weber, P.: Semantic degrees for industrie 4.0. CoRR, abs\/1505.05625 (2015)","key":"4_CR8"},{"unstructured":"Cheng, C., Shankar, N., Ruess, H., Bensalem, S.: EFSMT: a logical framework for cyber-physical systems. CoRR, abs\/1306.3456 (2013)","key":"4_CR9"},{"doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Parameter synthesis with IC3. In: FMCAD, pp. 165\u2013168. IEEE (2013)","key":"4_CR10","DOI":"10.1109\/FMCAD.2013.6679406"},{"key":"4_CR11","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 (1992)","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"4_CR12","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s11786-011-0098-x","volume":"5","author":"W Damm","year":"2011","unstructured":"Damm, W., Ihlemann, C., Sofronie-Stokkermans, V.: Ptime parametric verification of safety properties for reasonable linear hybrid automata. Math. Comput. Sci. 5(4), 469 (2011)","journal-title":"Math. Comput. Sci."},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-19249-9_14","volume-title":"FM 2015: Formal Methods","author":"T Dang","year":"2015","unstructured":"Dang, T., Dreossi, T., Piazza, C.: Parameter synthesis through temporal logic specifications. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 213\u2013230. Springer, Heidelberg (2015). doi:\n                      10.1007\/978-3-319-19249-9_14"},{"key":"4_CR14","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). doi:\n                      10.1007\/978-3-642-14295-6_17"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-642-16265-7_12","volume-title":"Integrated Formal Methods","author":"J Faber","year":"2010","unstructured":"Faber, J., Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: Automatic verification of parametric specifications with complex topologies. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 152\u2013167. Springer, Heidelberg (2010). doi:\n                      10.1007\/978-3-642-16265-7_12"},{"issue":"5\u20136","key":"4_CR16","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5\u20136), 519\u2013539 (2013)","journal-title":"STTT"},{"key":"4_CR17","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). doi:\n                      10.1007\/978-3-540-78929-1_14"},{"key":"4_CR18","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 (2013)","journal-title":"Int. J. Found. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Wong-Toi, H.: Using HyTech to synthesize control parameters for a steam boiler. In: FMIA (1995)","key":"4_CR19","DOI":"10.1007\/BFb0027241"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52","author":"T Hune","year":"2002","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52, 183 (2002)","journal-title":"J. Log. Algebr. Program."},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-642-36742-7_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 401\u2013415. Springer, Heidelberg (2013). doi:\n                      10.1007\/978-3-642-36742-7_28"},{"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)","key":"4_CR22","DOI":"10.1109\/ACSD.2013.11"},{"key":"4_CR23","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 Moura","year":"2007","unstructured":"Moura, L., Bj\u00f8rner, N.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007). doi:\n                      10.1007\/978-3-540-73595-3_13"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/3-540-45620-1_35","volume-title":"Automated Deduction\u2014CADE-18","author":"L Moura","year":"2002","unstructured":"Moura, L., Rue\u00df, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 438\u2013455. Springer, Heidelberg (2002). doi:\n                      10.1007\/3-540-45620-1_35"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-14203-1_15","volume-title":"Automated Reasoning","author":"V Sofronie-Stokkermans","year":"2010","unstructured":"Sofronie-Stokkermans, V.: Hierarchical reasoning for the verification of parametric systems. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 171\u2013187. Springer, Heidelberg (2010). doi:\n                      10.1007\/978-3-642-14203-1_15"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-27813-9_23","volume-title":"Computer Aided Verification","author":"F Wang","year":"2004","unstructured":"Wang, F.: Symbolic parametric safety analysis of linear hybrid systems with BDD-like data-structures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 295\u2013307. Springer, Heidelberg (2004). doi:\n                      10.1007\/978-3-540-27813-9_23"}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:13:56Z","timestamp":1558314836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_4","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":"8 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 November 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fm2016.cs.ucy.ac.cy\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}