{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:24Z","timestamp":1750219824885,"version":"3.41.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2023,9,9]],"date-time":"2023-09-09T00:00:00Z","timestamp":1694217600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Defense Innovation Agency (AID) of the French Ministry of Defense","award":["CLEDESCHAMPS N 2021 65 0070"],"award-info":[{"award-number":["CLEDESCHAMPS N 2021 65 0070"]}]},{"name":"Defense Innovation Agency (AID) of the French Ministry of Defense","award":["CLEDESCHAMPS N 2021 65 0070"],"award-info":[{"award-number":["CLEDESCHAMPS N 2021 65 0070"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2023,10,31]]},"abstract":"<jats:p>Model-based design tools like SCADE Suite and Simulink are often used to design safety-critical embedded software. Consequently, generating correct code from such models is crucial. We tackle this challenge on Lustre, a dataflow synchronous language that embodies the concepts that base such tools. Instead of proving correct a whole code generator, we turn an existing compiler into a certifying compiler from Lustre to C, following a translation validation approach.<\/jats:p>\n          <jats:p>We propose a solution that generates both C code and an attached specification expressing a correctness result for the generated and optionally optimized code. The specification yields proof obligations that are discharged by external solvers through the Frama-C platform.<\/jats:p>","DOI":"10.1145\/3609393","type":"journal-article","created":{"date-parts":[[2023,9,9]],"date-time":"2023-09-09T13:33:18Z","timestamp":1694266398000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation"],"prefix":"10.1145","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0642-6008","authenticated-orcid":false,"given":"L\u00e9lio","family":"Brun","sequence":"first","affiliation":[{"name":"National Institute of Informatics, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4467-2939","authenticated-orcid":false,"given":"Christophe","family":"Garion","sequence":"additional","affiliation":[{"name":"ISAE-SUPAERO, University of Toulouse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0513-6076","authenticated-orcid":false,"given":"Pierre-Lo\u00efc","family":"Garoche","sequence":"additional","affiliation":[{"name":"ENAC, University of Toulouse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-1126-6835","authenticated-orcid":false,"given":"Xavier","family":"Thirioux","sequence":"additional","affiliation":[{"name":"ISAE-SUPAERO, University of Toulouse, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,9,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/1109\/SKG49510.2019.00034"},{"key":"e_1_3_1_3_2","unstructured":"ANSYS. 2021. SCADE Suite. (2021). https:\/\/www.ansys.com\/products\/embedded-software\/ansys-scade-suite"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/978-3-642-16256-5_6"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/978-3-642-22110-1_14"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3470569"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1109\/JPROC.2002.805826"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1109\/9.53519"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375657.1375674"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192406"},{"key":"e_1_3_1_11_2","volume-title":"Embedded Real Time Systems (ERTS) 2020 (ERTS\u201920)","author":"Bourbouh Hamza","year":"2020","unstructured":"Hamza Bourbouh, Pierre-Lo\u00efc Garoche, Thomas Loquen, Eric Noulard, and Claire Pagetti. 2020. CoCoSim, a code generation framework for control\/command applications: An overview of CoCoSim for multi-periodic discrete simulink models. In Embedded Real Time Systems (ERTS) 2020 (ERTS\u201920)."},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062358"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371112"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477041"},{"key":"e_1_3_1_15_2","unstructured":"L\u00e9lio Brun. Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset. (n.d.). https:\/\/www.leliobrun.net\/files\/thesis.pdf"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594301"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/780732.780754"},{"key":"e_1_3_1_18_2","volume-title":"In 14th Symposium on Principles of Programming Languages (POPL\u201987). ACM (POPL\u201987)","author":"Caspi Paul","year":"1987","unstructured":"Paul Caspi, Daniel Pilaud, Nicolas Halbwachs, and John Alexander Plaice. 1987. LUSTRE: A declarative language for programming synchronous systems. In In 14th Symposium on Principles of Programming Languages (POPL\u201987). ACM (POPL\u201987)."},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/s00165-010-0170-3"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/978-3-319-41540-6_29"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/978-3-319-19195-9_5"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/978-3-319-48628-4_3"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1109\/TASE.2017.8285623"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/978-3-540-45212-6_10"},{"key":"e_1_3_1_25_2","volume-title":"SMT Workshop: International Workshop on Satisfiability modulo Theories","author":"Conchon Sylvain","year":"2018","unstructured":"Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. 2018. Alt-ergo 2.2. In SMT Workshop: International Workshop on Satisfiability modulo Theories. Oxford, United Kingdom."},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"volume-title":"Heptagon\/BZR Manual","author":"Delaval Gwena\u00ebl","key":"e_1_3_1_27_2","unstructured":"Gwena\u00ebl Delaval, Adrien Guatto, Herv\u00e9 Marchand, Marc Pouzet, and Rutten \u00c9ric. Heptagon\/BZR Manual. PARKAS (ENS) and Ctrl-A (LIG\/Inria). https:\/\/gitlab.inria.fr\/synchrone\/heptagon\/-\/blob\/master\/manual\/heptagon-manual.pdf"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/978-3-030-60508-7_24"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/4204\/EPTCS.169.4"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517439"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/351268.351300"},{"key":"e_1_3_1_32_2","volume-title":"The Lustre V6 Reference Manual","author":"Jahier Erwan","year":"2020","unstructured":"Erwan Jahier, Pascal Raymond, and Nicolas Halbwachs. 2020. The Lustre V6 Reference Manual. Verimag. http:\/\/www-verimag.imag.fr\/DIST-TOOLS\/SYNCHRONE\/lustre-v6\/doc\/lv6-ref-man.pdf"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_34_2","unstructured":"Mathworks. 2021. Simulink. (2021). https:\/\/www.mathworks.com\/products\/simulink"},{"key":"e_1_3_1_35_2","first-page":"151","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science)","author":"Pnueli Amir","year":"1998","unstructured":"Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science), Bernhard Steffen (Ed.). Springer, Berlin, 151\u2013166."},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.5555\/646252.686146"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/3-540-48092-7_11"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/978-3-642-02658-4_57"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/1017753.1017795"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/1109\/ICSE-C.2017.83"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/s11432-016-9270-0"},{"key":"e_1_3_1_42_2","unstructured":"The Coq Team. 2021. Coq. (2021). https:\/\/coq.inria.fr"},{"key":"e_1_3_1_43_2","unstructured":"Xavier Thirioux and Pierre-Lo\u00efc Garoche. 2021. LustreC. (2021). https:\/\/github.com\/Embedded-SW-VnV\/lustrec"},{"key":"e_1_3_1_44_2","volume-title":"ERTS2 2010, Embedded Real Time Software & Systems","author":"Toom Andres","year":"2010","unstructured":"Andres Toom, Nassima Izerrouken, T\u00f5nu N\u00e4ks, Marc Pantel, and Olivier Ssi Yan Kai. 2010. Towards reliable code generation with an open tool: Evolutions of the gene-auto toolset. In ERTS2 2010, Embedded Real Time Software & Systems. Toulouse, France."},{"key":"e_1_3_1_45_2","volume-title":"Embedded Real Time Software and Systems (ERTS2008\u201908)","author":"Toom Andres","year":"2008","unstructured":"Andres Toom, T\u00f5nu N\u00e4ks, Marc Pantel, Marcel Gandriau, and I. Wati. 2008. Gene-auto: An automatic code generator for a safe subset of simulink\/stateflow and scicos. In Embedded Real Time Software and Systems (ERTS2008\u201908). Toulouse, France."},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/1113830.1113834"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/s11704-015-4364-y"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007\/978-3-319-24953-7_33"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658587"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609393","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3609393","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:23Z","timestamp":1750178783000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609393"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,9]]},"references-count":48,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2023,10,31]]}},"alternative-id":["10.1145\/3609393"],"URL":"https:\/\/doi.org\/10.1145\/3609393","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2023,9,9]]},"assertion":[{"value":"2023-03-23","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-07-13","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}