{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:31Z","timestamp":1750221271382,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,9,29]],"date-time":"2017-09-29T00:00:00Z","timestamp":1506643200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,9,29]]},"DOI":"10.1145\/3127041.3127056","type":"proceedings-article","created":{"date-parts":[[2017,9,27]],"date-time":"2017-09-27T12:34:00Z","timestamp":1506515640000},"page":"165-174","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A refinement-based compiler development for synchronous languages"],"prefix":"10.1145","author":[{"given":"Jean-Paul","family":"Bodeveix","sequence":"first","affiliation":[{"name":"IRIT Universit\u00e9 Paul Sabatier, Toulouse, France"}]},{"given":"Mamoun","family":"Filali-Amine","sequence":"additional","affiliation":[{"name":"IRIT CNRS, Toulouse, France"}]},{"given":"Shuanglong","family":"Kan","sequence":"additional","affiliation":[{"name":"Nanjing University of Aeronautics and Astronautics, Nanjing, China"}]}],"member":"320","published-online":{"date-parts":[[2017,9,29]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Modeling in Event-B - System and Software Engineering","author":"Abrial Jean-Raymond","year":"1895","unstructured":"Jean-Raymond Abrial . 2010. Modeling in Event-B - System and Software Engineering . Cambridge University Press . http:\/\/www.cambridge.org\/uk\/catalogue\/catalogue.asp?isbn=978052 1895 569 Jean-Raymond Abrial. 2010. Modeling in Event-B - System and Software Engineering. Cambridge University Press. http:\/\/www.cambridge.org\/uk\/catalogue\/catalogue.asp?isbn=9780521895569"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0238-x"},{"volume-title":"Finite transition systems - semantics of communicating systems","author":"Arnold Andr\u00e9","key":"e_1_3_2_1_4_1","unstructured":"Andr\u00e9 Arnold . 1994. Finite transition systems - semantics of communicating systems . Prentice Hall . Andr\u00e9 Arnold. 1994. Finite transition systems - semantics of communicating systems. Prentice Hall."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375657.1375674"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-011-0177-4"},{"volume-title":"Reactive Specification","author":"Gamati\u00e9 Abdoulaye","key":"e_1_3_2_1_8_1","unstructured":"Abdoulaye Gamati\u00e9 . 2010. Designing Embedded Systems with the SIGNAL Programming Language - Synchronous , Reactive Specification . Springer . Abdoulaye Gamati\u00e9. 2010. Designing Embedded Systems with the SIGNAL Programming Language - Synchronous, Reactive Specification. Springer."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10373-5_27"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"volume-title":"Communication and Concurrency","author":"Milner R.","key":"e_1_3_2_1_12_1","unstructured":"R. Milner . 1989. Communication and Concurrency . Prentice-Hall, Inc. , Upper Saddle River, NJ, USA. R. Milner. 1989. Communication and Concurrency. Prentice-Hall, Inc., Upper Saddle River, NJ, USA."},{"key":"e_1_3_2_1_13_1","volume-title":"FORTE","author":"Ngo Van Chan","year":"2015","unstructured":"Van Chan Ngo , Jean-Pierre Talpin , and Thierry Gautier . 2015. Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler . In FORTE , Grenoble, France , June 2--4, 2015 (LNCS), Susanne Graf and Mahesh Viswanathan (Eds.), Vol. 9039 . Springer , 66--80. Van Chan Ngo, Jean-Pierre Talpin, and Thierry Gautier. 2015. Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler. In FORTE, Grenoble, France, June 2--4, 2015 (LNCS), Susanne Graf and Mahesh Viswanathan (Eds.), Vol. 9039. Springer, 66--80."},{"key":"e_1_3_2_1_14_1","volume-title":"Paulson","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow , Markus Wenzel , and Lawrence C . Paulson . 2002 . Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag , Berlin, Heidelberg. Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin, Heidelberg."},{"key":"e_1_3_2_1_15_1","volume-title":"PVS: A Prototype Verification System. In 11th International Conference on Automated Deduction (LNAI), Deepak Kapur (Ed.)","volume":"607","author":"Owre S.","unstructured":"S. Owre , J. M. Rushby , and N. Shankar . 1992 . PVS: A Prototype Verification System. In 11th International Conference on Automated Deduction (LNAI), Deepak Kapur (Ed.) , Vol. 607 . Springer-Verlag, Saratoga, NY, 748--752. S. Owre, J. M. Rushby, and N. Shankar. 1992. PVS: A Prototype Verification System. In 11th International Conference on Automated Deduction (LNAI), Deepak Kapur (Ed.), Vol. 607. Springer-Verlag, Saratoga, NY, 748--752."},{"key":"e_1_3_2_1_16_1","volume-title":"Translation Validation: From SIGNAL to C. In Correct System Design, Recent Insight and Advances (LNCS), Ernst-R\u00fcdiger Olderog and Bernhard Steffen (Eds.)","author":"Pnueli Amir","year":"1999","unstructured":"Amir Pnueli , Ofer Strichman , and Michael Siegel . 1999 . Translation Validation: From SIGNAL to C. In Correct System Design, Recent Insight and Advances (LNCS), Ernst-R\u00fcdiger Olderog and Bernhard Steffen (Eds.) , Vol. 1710 . Springer , 231--255. Amir Pnueli, Ofer Strichman, and Michael Siegel. 1999. Translation Validation: From SIGNAL to C. In Correct System Design, Recent Insight and Advances (LNCS), Ernst-R\u00fcdiger Olderog and Bernhard Steffen (Eds.), Vol. 1710. Springer, 231--255."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-7844-8"},{"key":"e_1_3_2_1_18_1","unstructured":"Rodin {n. d.}. http:\/\/www.event-b.org\/. ({n. d.}).  Rodin {n. d.}. http:\/\/www.event-b.org\/. ({n. d.})."},{"key":"e_1_3_2_1_19_1","volume-title":"15th Int. Conference","volume":"2410","author":"Schneider Klaus","year":"2002","unstructured":"Klaus Schneider . 2002 . Proving the Equivalence of Microstep and Macrostep Semantics. In Theorem Proving in Higher Order Logics , 15th Int. Conference , Hampton, VA, USA, August 20--23 (LNCS), Victor Carre\u00f1o, C\u00e9sar A. Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.) , Vol. 2410 . Springer, 314--331. Klaus Schneider. 2002. Proving the Equivalence of Microstep and Macrostep Semantics. In Theorem Proving in Higher Order Logics, 15th Int. Conference, Hampton, VA, USA, August 20--23 (LNCS), Victor Carre\u00f1o, C\u00e9sar A. Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.), Vol. 2410. Springer, 314--331."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.028"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.04.009"}],"event":{"name":"MEMOCODE '17: 15th ACM-IEEE International Conference on Formal Methods and Models for System Design","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA"],"location":"Vienna Austria","acronym":"MEMOCODE '17"},"container-title":["Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127041.3127056","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3127041.3127056","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:06Z","timestamp":1750212666000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127041.3127056"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,29]]},"references-count":19,"alternative-id":["10.1145\/3127041.3127056","10.1145\/3127041"],"URL":"https:\/\/doi.org\/10.1145\/3127041.3127056","relation":{},"subject":[],"published":{"date-parts":[[2017,9,29]]},"assertion":[{"value":"2017-09-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}