PhD Thesis: Formal and Executable Specification of Domain-Specific Language Families

We are looking for a highly motivated student who wish to conduct research studies in language engineering. The main objective of the proposed PhD programme is to integrate the efficient and modular implementation patterns for languages, with a formal framework such as the K framework. The ultimate goal is to offer an integrated language specification environment supporting formal reuse of language modules, such as new languages can be built by composition and configuration of existing modules, or specified in terms of existing modules.


The main advisor of the PhD thesis will be Prof. Benoit Combemale (University of Toulouse & Inria, DiverSE team), and the co-supervisors will be Olivier Barais (Univ. Rennes 1) and Gurvan Leguernic (DGA).


  • K Overview and SIMPLE Case Study. Grigore Rosu and Traian Florin Serbanuta. K’11, ENTCS 304, pp 3-56. 2014
  • The K Primer (version 3.3). Traian Florin Serbanuta and Andrei Arusoaie and David Lazar and Chucky Ellison and Dorel Lucanu and Grigore Rosu. K’11, ENTCS 304, pp 57-80. 2014
  • An Executable Formal Semantics of C with Applications. Chucky Ellison and Grigore Rosu. POPL’12, ACM, pp 533-544. 2012
  • Programming Language Semantics. Schmidt, David A. CRC/ACM Computer Science Handbook, 3d ed., 2014.
  • Meaningful modeling: what’s the semantics of semantics? D. Harel and B. Rumpe, Computer, vol. 37, no. 10, pp. 64– 72, 2004.
  • Model-Based Language Engineering with EMFText. Florian Heidenreich, Jendrik Johannes, Sven Karol, Mirko Seifert and Christian Wende. International Summer School Generative and Transformational Techniques in Software Engineering IV, 2013.
  • Model-driven Language Engineering: the ASMETA case study. Angelo Gargantin, Elvinia Riccobene and Patrizia Scandurra. ICSEA 2008.
  • Thomas Degueule, Benoit Combemale, Arnaud Blouin, Olivier Barais, Jean-Marc Jézéquel: Melange: A Meta-language for Modular and Reusable Development of DSLs, SLE 2015, ACM, 2015.
  • Edoardo Vacchi, Walter Cazzola, Benoît Combemale, Mathieu Acher: Automating variability model inference for component-based language implementations. SPLC 2014: 167-176
  • Edoardo Vacchi, Walter Cazzola, Suresh Pillay, Benoît Combemale: Variability Support in Domain-Specific Language Development. SLE 2013: 76-95
  • Jean-Marc Jézéquel, Benoit Combemale, Olivier Barais, Martin Monperrus, François Fouquet. Mashup of Meta-Languages and its Implementation in the Kermeta Language Workbench. Software and Systems Modeling, Springer Verlag, 2015, 14 (2), pp.905-920.
  • Mounira Kezadri, Marc Pantel, Benoit Combemale, Xavier Thirioux. A formal framework to prove the correctness of model driven engineering composition operators. ICFEM’14 - 16TH INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, Nov 2014, Luxembourg, Luxembourg. Springer, 2014.
  • Benoît Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux: Essay on Semantics Definition in MDE - An Instrumented Approach for Model Verification. JSW 4(9): 943-958 (2009)
  • Benoît Combemale, Jörg Kienzle, Gunter Mussbacher, Olivier Barais, Erwan Bousse, Walter Cazzola, Philippe Collet, Thomas Degueule, Robert Heinrich, Jean-Marc Jézéquel, Manuel Leduc, Tanja Mayerhofer, Sébastien Mosser, Matthias Schöttle, Misha Strittmatter, Andreas Wortmann: Concern-oriented language development (COLD): Fostering reuse in language engineering. Computer Languages, Systems & Structures 54: 139-155 (2018)
  • Manuel Leduc, Thomas Degueule, Benoît Combemale: Modular language composition for the masses. SLE 2018: 47-59
  • Manuel Leduc, Thomas Degueule, Benoît Combemale, Tijs van der Storm, Olivier Barais: Revisiting Visitors for Modular Extension of Executable DSMLs. MoDELS 2017: 112-122
  • Gurvan Le Guernic, Benoît Combemale, José A. Galindo: Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework. F-IDE@FM 2016: 38-52