{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:15:39Z","timestamp":1750306539412,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,6,1]],"date-time":"2015-06-01T00:00:00Z","timestamp":1433116800000},"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":[[2015,6]]},"DOI":"10.1145\/2764967.2775291","type":"proceedings-article","created":{"date-parts":[[2015,7,6]],"date-time":"2015-07-06T14:04:29Z","timestamp":1436191469000},"page":"109-112","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools"],"prefix":"10.1145","author":[{"given":"Van-Chan","family":"Ngo","sequence":"first","affiliation":[{"name":"INRIA Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[{"name":"INRIA Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thierry","family":"Gautier","sequence":"additional","affiliation":[{"name":"INRIA Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lo\u00efc","family":"Besnard","sequence":"additional","affiliation":[{"name":"INRIA Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Le Guernic","sequence":"additional","affiliation":[{"name":"INRIA Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,6]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Astr\u00e9e http:\/\/www.astree.ens.fr.  Astr\u00e9e http:\/\/www.astree.ens.fr."},{"key":"e_1_3_2_1_2_1","volume-title":"The foundations of Esterel. Essay in Honor of Robin Milner","author":"Berry G.","year":"2000","unstructured":"G. Berry . The foundations of Esterel. Essay in Honor of Robin Milner , MIT Press , 2000 . G. Berry. The foundations of Esterel. Essay in Honor of Robin Milner, MIT Press, 2000."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_1_6_1","volume-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications. Model Checking","author":"Clarke E.M.","year":"2000","unstructured":"E.M. Clarke , O. Grumberg , and D.A. Peled . Automatic verification of finite-state concurrent systems using temporal logic specifications. Model Checking , The MIT Press , Cambridge, MA , 2000 . E.M. Clarke, O. Grumberg, and D.A. Peled. Automatic verification of finite-state concurrent systems using temporal logic specifications. Model Checking, The MIT Press, Cambridge, MA, 2000."},{"key":"e_1_3_2_1_7_1","unstructured":"Inria The CompCert Project. http:\/\/compcert.inria.fr.  Inria The CompCert Project. http:\/\/compcert.inria.fr."},{"key":"e_1_3_2_1_8_1","volume-title":"Engineering a Compiler","author":"Cooper K.","year":"2011","unstructured":"K. Cooper and L. Torczon . Engineering a Compiler , Second Edition. Morgan Kaufmann , 2011 . K. Cooper and L. Torczon. Engineering a Compiler, Second Edition. Morgan Kaufmann, 2011."},{"key":"e_1_3_2_1_9_1","unstructured":"Coq-Inria. Coq proof assistant. http:\/\/coq.inria.fr.  Coq-Inria. Coq proof assistant. http:\/\/coq.inria.fr."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008649901864"},{"key":"e_1_3_2_1_11_1","unstructured":"The Yices Sat-solver. http:\/\/yices.csl.ri.com.  The Yices Sat-solver. http:\/\/yices.csl.ri.com."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1967677.1967688"},{"key":"e_1_3_2_1_13_1","volume-title":"Introduction to HOL: A theorem proving environment for higher order logic","author":"Gordon J.C.","year":"1993","unstructured":"M. J.C. Gordon and T.F. Melham . Introduction to HOL: A theorem proving environment for higher order logic . Cambridge University Press , 1993 . M.J.C. Gordon and T.F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of the IEEE Special Issue","author":"Le Guernic P.","year":"1991","unstructured":"P. Le Guernic , M. Le Borgne , T. Gautier , and C. Le Maire . Programming real-time applications with Signal . Proceedings of the IEEE Special Issue , 1991 . P. Le Guernic, M. Le Borgne, T. Gautier, and C. Le Maire. Programming real-time applications with Signal. Proceedings of the IEEE Special Issue, 1991."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2005.1487884"},{"key":"e_1_3_2_1_16_1","unstructured":"The Isabelle proof assistant. http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle.  The Isabelle proof assistant. http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498765.1498787"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30729-4_9"},{"key":"e_1_3_2_1_22_1","volume-title":"Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler. International Conference on Formal Techniques for Distributed Objects, Components and Systems. IFIP","author":"Ngo V. C.","year":"2015","unstructured":"V. C. Ngo , J.-P. Talpin , T. Gautier . Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler. International Conference on Formal Techniques for Distributed Objects, Components and Systems. IFIP , 2015 . V. C. Ngo, J.-P. Talpin, T. Gautier. Translation Validation for Synchronous Data-flow Specification in the SIGNAL Compiler. International Conference on Formal Techniques for Distributed Objects, Components and Systems. IFIP, 2015."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46675-9_12"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ESLsyn.2014.6850379"},{"key":"e_1_3_2_1_25_1","unstructured":"Polarsys project POP Polychrony On Polarsys. https:\/\/www.polarsys.org\/projects\/polarsys.pop.  Polarsys project POP Polychrony On Polarsys. https:\/\/www.polarsys.org\/projects\/polarsys.pop."},{"key":"e_1_3_2_1_26_1","volume-title":"Translation Validation. International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer","author":"Pnueli A.","year":"1998","unstructured":"A. Pnueli , M. Siegel , and E. Singerman , Translation Validation. International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer , 1998 . A. Pnueli, M. Siegel, and E. Singerman, Translation Validation. International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 1998."},{"key":"e_1_3_2_1_27_1","volume-title":"LNCS 1710","author":"Pnueli A.","year":"2000","unstructured":"A. Pnueli , O. Shtrichman , and M. Siegel , Translation Validation: From Signal to C. Correct System Design Recent Insights and Advances , LNCS 1710 , Springer , 2000 . A. Pnueli, O. Shtrichman, and M. Siegel, Translation Validation: From Signal to C. Correct System Design Recent Insights and Advances, LNCS 1710, Springer, 2000."},{"key":"e_1_3_2_1_28_1","volume-title":"ACM Symposium on Principles of Programming Languages","author":"Quielle J.P.","year":"1981","unstructured":"J.P. Quielle and J. Sifakis . Specification and verification of concurrent systems in Cesar . ACM Symposium on Principles of Programming Languages , 1981 . J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in Cesar. ACM Symposium on Principles of Programming Languages, 1981."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038675"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993533"}],"event":{"name":"SCOPES '15: 18th International Workshop on Software and Compilers for Embedded Systems","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","EDAA European Design Automation Association"],"location":"Sankt Goar Germany","acronym":"SCOPES '15"},"container-title":["Proceedings of the 18th International Workshop on Software and Compilers for Embedded Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2764967.2775291","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2764967.2775291","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:12:24Z","timestamp":1750227144000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2764967.2775291"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6]]},"references-count":30,"alternative-id":["10.1145\/2764967.2775291","10.1145\/2764967"],"URL":"https:\/\/doi.org\/10.1145\/2764967.2775291","relation":{},"subject":[],"published":{"date-parts":[[2015,6]]},"assertion":[{"value":"2015-06-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}