OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

A Refinement-based compiler development for synchronous languages

Bodeveix, Jean-Paul and Filali, Mamoun and Shuanglong, Kan A Refinement-based compiler development for synchronous languages. (2017) In: 15th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE 2017), 29 September 2017 - 2 October 2017 (Vienna, Austria).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://doi.org/10.1145/3127041.3127056


In this paper, we are concerned by the elaboration of generic development steps for the code generation for synchronous languages. Our aim is to provide a correct by construction solution. For that purpose, we adopt a refinement-based approach where proof obligations for each step guarantee properties preservation. We use the Event-B formal method. We start with a big step semantics specified by an Event-B machine. Through a sequence of refinements, expressed as Event-B refinement machines, we end up with a code generation step which implements a small step semantics preserving the properties of the big step semantics.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to ACM. The definitive version is available at http://dl.acm.org This papers appears in MEMOCODE'17 ISBN: 978-1-4503-5093-8 The original PDF is available at: https://dl.acm.org/citation.cfm?doid=3127041.3127056
HAL Id:hal-03624681
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Nanjing University of Aeronautics and Astronautics – NUAA (CHINA)
Laboratory name:
Deposited On:17 Oct 2018 09:58

Repository Staff Only: item control page