{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:05:20Z","timestamp":1762459520406,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319670881"},{"type":"electronic","value":"9783319670898"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-67089-8_4","type":"book-chapter","created":{"date-parts":[[2017,8,24]],"date-time":"2017-08-24T12:47:26Z","timestamp":1503578846000},"page":"42-58","source":"Crossref","is-referenced-by-count":7,"title":["Refinement of Trace Abstraction for Real-Time Programs"],"prefix":"10.1007","author":[{"given":"Franck","family":"Cassez","sequence":"first","affiliation":[]},{"given":"Peter Gj\u00f8l","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"Kim","family":"Guldstrand Larsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,25]]},"reference":[{"issue":"2","key":"4_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-32759-9_6","volume-title":"FM 2012: Formal Methods","author":"\u00c9 Andr\u00e9","year":"2012","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., K\u00fchne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33\u201336. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32759-9_6"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-17524-9_5","volume-title":"NASA Formal Methods","author":"\u00c9 Andr\u00e9","year":"2015","unstructured":"Andr\u00e9, \u00c9., Lipari, G., Nguyen, H.G., Sun, Y.: Reachability preservation based parameter synthesis for timed automata. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 50\u201365. Springer, Cham (2015). doi: 10.1007\/978-3-319-17524-9_5"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST 2006, pp. 125\u2013126 (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11603009_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"B B\u00e9rard","year":"2005","unstructured":"B\u00e9rard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the expressiveness of timed automata and time Petri nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 211\u2013225. Springer, Heidelberg (2005). doi: 10.1007\/11603009_17"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-28756-5_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2012","unstructured":"Beyer, D.: Competition on software verification. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 504\u2013524. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_38"},{"key":"4_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2012.12.005","volume":"474","author":"B B\u00e9rard","year":"2013","unstructured":"B\u00e9rard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: The expressive power of time Petri nets. Theor. Comput. Sci. 474, 1\u201320 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Byg, J., Jacobsen, M., Jacobsen, L., J\u00f8rgensen, K.Y., M\u00f8ller, M.H., Srba, J.: TCTL-preserving translations from timed-arc Petri nets to networks of timed automata. TCS (2013). doi: 10.1016\/j.tcs.2013.07.011","DOI":"10.1016\/j.tcs.2013.07.011"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-44618-4_12","volume-title":"CONCUR 2000 \u2014 Concurrency Theory","author":"F Cassez","year":"2000","unstructured":"Cassez, F., Larsen, K.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 138\u2013152. Springer, Heidelberg (2000). doi: 10.1007\/3-540-44618-4_12"},{"issue":"10","key":"4_CR10","doi-asserted-by":"crossref","first-page":"1456","DOI":"10.1016\/j.jss.2005.12.021","volume":"79","author":"F Cassez","year":"2006","unstructured":"Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. J. Softw. Syst. 79(10), 1456\u20131468 (2006)","journal-title":"J. Softw. Syst."},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-662-54580-5_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Cassez","year":"2017","unstructured":"Cassez, F., Sloane, A.M., Roberts, M., Pigram, M., Suvanpong, P., de Aledo, P.G.: Skink: static analysis of programs in LLVM intermediate representation - (Competition Contribution). In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 380\u2013384. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54580-5_27"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). doi: 10.1007\/10722167_15"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-75454-1_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"H Dierks","year":"2007","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114\u2013129. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75454-1_10"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258\u2013273. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-31954-2_17"},{"key":"4_CR16","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., 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). doi: 10.1007\/978-3-642-22110-1_30"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-03237-0_7","volume-title":"Static Analysis","author":"M Heizmann","year":"2009","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69\u201385. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03237-0_7"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_2"},{"key":"4_CR19","first-page":"460","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-toi, H.: HyTech: a model checker for hybrid systems. Softw. Tools Technol. Transf. 1, 460\u2013463 (1997)","journal-title":"Softw. Tools Technol. Transf."},{"issue":"1","key":"4_CR20","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-319-06410-9_25","volume-title":"FM 2014: Formal Methods","author":"P Kordy","year":"2014","unstructured":"Kordy, P., Langerak, R., Mauw, S., Polderman, J.W.: A symbolic algorithm for the analysis of robust timed automata. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 351\u2013366. Springer, Cham (2014). doi: 10.1007\/978-3-319-06410-9_25"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-662-46681-0_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Sankur","year":"2015","unstructured":"Sankur, O.: Symbolic quantitative robustness analysis of timed automata. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 484\u2013498. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_48"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-319-11936-6_28","volume-title":"Automated Technology for Verification and Analysis","author":"W Wang","year":"2014","unstructured":"Wang, W., Jiao, L.: Trace abstraction refinement for timed automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 396\u2013410. Springer, Cham (2014). doi: 10.1007\/978-3-319-11936-6_28"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67089-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T01:29:32Z","timestamp":1750814972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67089-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319670881","9783319670898"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67089-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}