{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T17:28:23Z","timestamp":1775323703548,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030022143","type":"print"},{"value":"9783030022150","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,12,20]],"date-time":"2018-12-20T00:00:00Z","timestamp":1545264000000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-02215-0_3","type":"book-chapter","created":{"date-parts":[[2018,12,19]],"date-time":"2018-12-19T00:01:12Z","timestamp":1545177672000},"page":"45-70","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Simulation of Dataflow Synchronous Programs with Timers"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Baudart","sequence":"first","affiliation":[]},{"given":"Timothy","family":"Bourke","sequence":"additional","affiliation":[]},{"given":"Marc","family":"Pouzet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,12,20]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, Formal verification of hybrid systems, in International Conference on Embedded Software (EMSOFT), Taiwan, Oct 2011, pp. 273\u2013278","DOI":"10.1145\/2038642.2038685"},{"issue":"2","key":"3_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"R. Alur, D.L. Dill, A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR3","unstructured":"G. Baudart, A Synchronous Approach to Quasi-Periodic Systems. Ph.D. thesis, PSL Research University, Mar 2017"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"K. Bauer, K. Schneider From synchronous programs to symbolic representations of hybrid systems, in International Conference on Hybrid Systems: Computation and Control (HSCC), Stockholm (ACM Press, Apr 2010), pp. 41\u201350","DOI":"10.1145\/1755952.1755960"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"G. Behrmann, A. David, K.G. Larsen, J. H\u00e5kansson, P. Pettersson, W. Yi, M. Hendriks, Uppaal 4.0, in International Conference on the Quantitative Evaluation of Systems (QEST), Riverside (IEEE Computing Society, Sept 2006), pp. 125\u2013126","DOI":"10.1109\/QEST.2006.59"},{"key":"3_CR6","unstructured":"J. Bengtsson, Clocks, DBMs and states in timed systems. Ph.D. thesis, Uppsala University (2002)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"A. Benveniste, T. Bourke, B. Caillaud, M. Pouzet, Divide and recycle: types and compilation for a hybrid synchronous language, in Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Chicago, Apr 2011, pp. 61\u201370","DOI":"10.1145\/1967677.1967687"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"A. Benveniste, T. Bourke, B. Caillaud, M. Pouzet, A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous code, in International Conference on Embedded Software (EMSOFT), Taiwan, Oct 2011","DOI":"10.1145\/2038642.2038664"},{"key":"3_CR9","unstructured":"B. Berthomieu, M. Menasche, An enumerative approach for analyzing Time Petri Nets, in World Computer Congress (IFIP), Sept 1983, pp. 41\u201346"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"V. Bertin, E. Closse, M. Poize, J. Pulou, J. Sifakis, P. Venier, D. Weil, S. Yovine, Taxys = Esterel + Kronos: a tool for verifying real-time properties of embedded systems, in CDC, Orlando (IEEE, Dec 2001), pp. 2875\u20132880","DOI":"10.1109\/CDC.2001.980712"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"T. Bourke, M. Pouzet, Z\u00e9lus: a synchronous language with ODEs, in International Conference on Hybrid Systems: Computation and Control (HSCC), Philadelphia, Apr 2013, pp. 113\u2013118","DOI":"10.1145\/2461328.2461348"},{"key":"3_CR12","unstructured":"P. Caspi, The quasi-synchronous approach to distributed control systems. Technical Report CMA\/009931, VERIMAG, Crysis Project, May 2000. The Cooking Book"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"P. Caspi, D. Pilaud, N. Halbwachs, J. Plaice, Lustre: a declarative language for programming synchronous systems, in Symposium on Principles of Programming Languages (POPL), Germany, Jan 1987, pp. 178\u2013188","DOI":"10.1145\/41625.41641"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-44618-4_12","volume-title":"CONCUR 2000 \u2014 Concurrency Theory","author":"Franck Cassez","year":"2000","unstructured":"F. Cassez, K.G. Larsen, The impressive power of stopwatches, in International Conference on Concurrency Theory (CONCUR), State College, Aug 2000, pp. 138\u2013152"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"A. Champion, A. Mebsout, C. Sticksel, C. Tinelli, The Kind 2 model checker, in International Conference on Computer Aided Verification (CAV), Canada, July 2016, pp. 510\u2013517","DOI":"10.1007\/978-3-319-41540-6_29"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"David L. Dill","year":"1990","unstructured":"D.L. Dill, Timing assumptions and verification of finite-state concurrent systems, in International Workshop on Automatic Verification Methods for Finite State Systems (AVMFSS), France, June 1990, pp. 197\u2013212"},{"issue":"5","key":"3_CR17","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/S1571-0661(05)80436-0","volume":"65","author":"D Garriou","year":"2002","unstructured":"D. Garriou, Symbolic simulation of synchronous programs. Electron. Notes Theor. Comput. Sci. 65(5), 11\u201318 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Computer Aided Verification","author":"Nicolas Halbwachs","year":"1993","unstructured":"N. Halbwachs, Delay analysis in synchronous programs, in International Conference on Computer Aided Verification (CAV), Greece, June 1993, pp. 333\u2013346"},{"issue":"2","key":"3_CR19","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic model checking for real-time systems. Inf. Comput. 111(2), 192\u2013244 (1994)","journal-title":"Inf. Comput."},{"key":"3_CR20","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/978-3-319-11737-9_14","volume-title":"Formal Methods and Software Engineering","author":"Tobias Isenberg","year":"2014","unstructured":"T. Isenberg, H. Wehrheim, Timed automata verification via IC3 with zones, in International Conference on Formal Methods and Software Engineering (ICFEM). Lecture Notes in Computer Science, vol. 8829, Nov 2014, pp. 203\u2013218"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"M. Jourdan, F. Maraninchi, A. Olivero, Verifying quantitative real-time properties of synchronous programs, in International Conference on Computer Aided Verification (CAV), Greece, June 1993","DOI":"10.1007\/3-540-56922-7_29"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"R. Kindermann, T. Junttila, I. Niemel\u00e4, SMT-based induction methods for timed systems, in International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science, vol. 7595, Sept 2012, pp. 171\u2013187","DOI":"10.1007\/978-3-642-33365-1_13"},{"issue":"1\u20132","key":"3_CR23","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"K.G. Larsen, P. Pettersson, Y. Wang, Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transfer 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"3_CR24","unstructured":"G. Logothetis, K. Schneider, Extending synchronous languages for generating abstract real-time models, in Design, Automation, and Test in Europe (DATE), France, Mar 2002"},{"key":"3_CR25","unstructured":"C. Mauras, Symbolic simulation of interpreted automata, in International Workshop on Synchronous Programming (SYNCHRON), Germany, Dec 1996"},{"issue":"1","key":"3_CR26","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"A. Min\u00e9, The octagon abstract domain. Higher-Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"Higher-Order Symb. Comput."},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"G. Morb\u00e9, F. Pigorsch, C. Scholl, Fully symbolic model checking for timed automata, in International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 6806, July 2011, pp. 616\u2013632","DOI":"10.1007\/978-3-642-22110-1_50"},{"key":"3_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1155\/2008\/753821","volume":"2008","author":"P Raymond","year":"2008","unstructured":"P. Raymond, Y. Roux, E. Jahier, Lutin: a language for specifying and executing reactive scenarios. EURASIP J. Embed. Syst. 2008, 1\u201311, (2008)","journal-title":"EURASIP J. Embed. Syst."},{"issue":"4","key":"3_CR29","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2008.05.008","volume":"203","author":"P Raymond","year":"2008","unstructured":"P. Raymond, Y. Roux, E. Jahier, Specifying and executing reactive scenarios with Lutin. Electron. Notes Theor. Comput. Sci. 203(4), 19\u201334 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"4","key":"3_CR30","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s00165-006-0008-1","volume":"18","author":"FW Vaandrager","year":"2006","unstructured":"F.W. Vaandrager, A.L. de Groot, Analysis of a biphase mark protocol with Uppaal and PVS. Form. Asp. Comput. 18(4), 433\u2013458 (2006)","journal-title":"Form. Asp. Comput."},{"key":"3_CR31","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10009-003-0135-4","volume":"6","author":"F Wang","year":"2004","unstructured":"F. Wang, Efficient verification of timed automata with BDD-like data structures. Int. J. Softw. Tools Technol. Transfer 6, 77\u201397 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"1","key":"3_CR32","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"S. Yovine, Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transfer 1(1), 123\u2013133 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"}],"container-title":["Lecture Notes in Electrical Engineering","Languages, Design Methods, and Tools for Electronic System Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02215-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T16:19:11Z","timestamp":1775319551000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02215-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,20]]},"ISBN":["9783030022143","9783030022150"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02215-0_3","relation":{},"ISSN":["1876-1100","1876-1119"],"issn-type":[{"value":"1876-1100","type":"print"},{"value":"1876-1119","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12,20]]}}}