{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:13:43Z","timestamp":1770297223592,"version":"3.49.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030670665","type":"print"},{"value":"9783030670672","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-67067-2_19","type":"book-chapter","created":{"date-parts":[[2021,1,11]],"date-time":"2021-01-11T20:57:20Z","timestamp":1610398640000},"page":"417-440","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Synchronous Effects Logic for Temporal Verification of Pure Esterel"],"prefix":"10.1007","author":[{"given":"Yahui","family":"Song","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,12]]},"reference":[{"issue":"1","key":"19_CR1","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/2578855.2535862","volume":"49","author":"CJ Anderson","year":"2014","unstructured":"Anderson, C.J., et al.: NetKAT: semantic foundations for networks. ACM SIGPLAN Notices 49(1), 113\u2013126 (2014)","journal-title":"ACM SIGPLAN Notices"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/3-540-59042-0_96","volume-title":"STACS 95","author":"V Antimirov","year":"1995","unstructured":"Antimirov, V.: Partial derivatives of regular expressions and finite automata constructions. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 455\u2013466. Springer, Heidelberg (1995). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/3-540-59042-0_96"},{"issue":"1","key":"19_CR3","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(95)80024-4","volume":"143","author":"V Antimirov","year":"1995","unstructured":"Antimirov, V., Mosses, P.: Rewriting extended regular expressions. Theoret. Comput. Sci. 143(1), 51\u201372 (1995)","journal-title":"Theoret. Comput. Sci."},{"key":"19_CR4","unstructured":"Berry, G.: The constructive semantics of pure Esterel-draft version 3. Draft Version, 3 (1999)"},{"key":"19_CR5","unstructured":"Berry, G.: The Esterel v5 language primer: version v5\\_91. Centre de math\u00e9matiques appliqu\u00e9es, Ecole des mines and INRIA (2000)"},{"issue":"2","key":"19_CR6","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87\u2013152 (1992)","journal-title":"Sci. Comput. Program."},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Berry, G., Nicolas, C., Serrano, M.: Hiphop: a synchronous reactive extension for Hop. In: Proceedings of the 1st ACM SIGPLAN International Workshop on Programming Language and Systems Technologies for Internet Clients, pp. 49\u201356 (2011)","DOI":"10.1145\/2093328.2093337"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-22360-5_5","volume-title":"Implementation and Application of Automata","author":"S Broda","year":"2015","unstructured":"Broda, S., Cavadas, S., Ferreira, M., Moreira, N.: Deciding synchronous Kleene algebra with derivatives. In: Drewes, F. (ed.) CIAA 2015. LNCS, vol. 9223, pp. 49\u201362. Springer, Cham (2015). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-319-22360-5_5"},{"key":"19_CR9","doi-asserted-by":"publisher","unstructured":"Brotherston J.: Cyclic proofs for first-order logic with inductive definitions. In: Beckert B. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2005. LNCS, vol 3702. Springer, Heidelberg (2005). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/11554554_8","DOI":"10.1007\/11554554_8"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M De Wulf","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17\u201330. Springer, Heidelberg (2006). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/11817963_5"},{"key":"19_CR11","unstructured":"Edwards, S.A.: The Columbia Esterel Compiler (2006). https:\/\/2.zoppoz.workers.dev:443\/http\/www.cs.columbia.edu\/~sedwards\/cec\/"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Florence, S.P., You, S.H., Tov, J.A., Findler, R.B.: A calculus for Esterel: if can, can. if no can, no can. Proc. ACM Program. Lang. 3(POPL), 1\u201329 (2019)","DOI":"10.1145\/3290374"},{"key":"19_CR13","unstructured":"Gonthier, G.: S\u00e9mantiques et mod\u00e8les d\u2019ex\u00e9cution des langages r\u00e9actifs synchrones: application \u00e0 ESTEREL. Ph.D. thesis, Paris 11, (1988)"},{"issue":"6","key":"19_CR14","doi-asserted-by":"publisher","first-page":"1795","DOI":"10.1016\/j.jcss.2011.12.003","volume":"78","author":"D Hovland","year":"2012","unstructured":"Hovland, D.: The inclusion problem for regular expressions. J. Comput. Syst. Sci. 78(6), 1795\u20131813 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-60045-0_45","volume-title":"Computer Aided Verification","author":"LJ Jagadeesan","year":"1995","unstructured":"Jagadeesan, L.J., Puchol, C., Von Olnhausen, J.E.: Safety property verification of Esterel programs and applications to telecommunications software. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 127\u2013140. Springer, Heidelberg (1995). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/3-540-60045-0_45"},{"key":"19_CR16","unstructured":"Keil, M., Thiemann, P.: Symbolic solving of extended regular expression inequalities. arXiv preprint arXiv:1410.3227 (2014)"},{"issue":"11","key":"19_CR17","first-page":"1","volume":"14","author":"GK Palshikar","year":"2001","unstructured":"Palshikar, G.K.: An introduction to Esterel. Embed. Syst. Program. 14(11), 1\u201312 (2001)","journal-title":"Embed. Syst. Program."},{"issue":"7","key":"19_CR18","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1016\/j.jlap.2010.07.009","volume":"79","author":"C Prisacariu","year":"2010","unstructured":"Prisacariu, C.: Synchronous Kleene algebra. J. Logic Algebraic Program. 79(7), 608\u2013635 (2010)","journal-title":"J. Logic Algebraic Program."},{"key":"19_CR19","unstructured":"Song, Y.: Synced effects source code (2020). https:\/\/2.zoppoz.workers.dev:443\/https\/github.com\/songyahui\/SyncedEffects.git"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Song, Y., Chin, W.-N.: Automated temporal verification of integrated dependent effects. In: International Conference on Formal Engineering Methods (2020)","DOI":"10.1007\/978-3-030-63406-3_5"},{"key":"19_CR21","unstructured":"Song, Y., Chin, W.-N.:Technical report (2020). https:\/\/2.zoppoz.workers.dev:443\/https\/www.comp.nus.edu.sg\/~yahuis\/VMCAI2021.pdf"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709\u2013714. Springer, Heidelberg (2009). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-642-02658-4_59"},{"issue":"1","key":"19_CR23","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.entcs.2004.09.040","volume":"128","author":"O Tardieu","year":"2005","unstructured":"Tardieu, O.: A deterministic logical semantics for Esterel. Electron. Notes Theoret. Comput. Sci. 128(1), 103\u2013122 (2005)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Vidal, C., Berry, G., Serrano, M.: Hiphop. js: a language to orchestrate web applications. In: Proceedings of the 33rd Annual ACM Symposium on Applied Computing, pp. 2193\u20132195 (2018)","DOI":"10.1145\/3167132.3167440"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-67067-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T20:12:00Z","timestamp":1718050320000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/10.1007\/978-3-030-67067-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030670665","9783030670672"],"references-count":24,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-030-67067-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"12 January 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Copenhagen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 January 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2.zoppoz.workers.dev:443\/https\/popl21.sigplan.org\/home\/VMCAI-2021","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}