Topic T5D: Formal Methods

Summary

• Requested in 24/26 calls
• Requested in 19/19 pure calls (2008–2026 with the longest streak of 19 years)
• Primary tagged in 12/26 paper bundles
• Primary tagged in 9/19 pure proceedings (2010–2025 with the longest streak of 3 years)
• Secondary tagged in 22/26 paper bundles
• Secondary tagged in 19/19 pure proceedings (2008–2026 with the longest streak of 19 years)
• Top 3 co-occurring topics:
  • T4A: Workbenches (30 times)
  • T3C: DSLs (14 times)
  • T1A: Design (13 times)
• Top 3 contributors:
  • Eric Van Wyk (6 times)
  • Martina Seidl (5 times)
  • Esther Guerra (4 times)

List of papers (76)

• (ATEM 2006 SI) Formalising Model Transformation Rules for UML/MOF 2 (Carsten Amelunxen, Andy Schürr) T3B T5D T3A T4A
• (ATEM 2006 SI) Evaluating Formal Properties of Feature Diagram Languages (Patrick Heymans, Pierre-Yves Schobbens, Jean-Christophe Trigaux, Yves Bontemps, Raimundas Matulevičius, Andreas Claßen) T2C T5D T1A T5B
• (SLE 2008) Analyzing Rule-Based Behavioral Semantics of Visual Modeling Languages with Maude (José Eduardo Rivera, Esther Guerra, Juan de Lara, Antonio Vallecillo) T1C T5D T4D
• (SLE 2008) Formalization and Rule-Based Transformation of EMF Ecore-Based Models (Bernhard Schätz) T4B T5D T3B
• (SLE 2009) Composing Feature Models (Mathieu Acher, Philippe Collet, Philippe Lahire, Robert B. France) T2C T1D T5D
• (SLE 2009) Model Transformation Languages Relying on Models as ADTs (Jerónimo Irazábal, Clàudia Pons) T3B T3A T5D
• (SLE 2009) Ontological Metamodeling with Explicit Instantiation (Alfons Laarman, Ivan Kurtev) T3E T3A T5D
• (SLE 2009) Verifiable Parse Table Composition for Deterministic Parsing (August Schwerdfeger, Eric Van Wyk) T1D T5D T4A
• (SLE 2010) Modelling GLL Parser Implementations (Adrian Johnstone, Elizabeth Scott) T4C T5F T5D
• (SLE 2010) DSLTrans: A Turing Incomplete Transformation Language (Bruno Barroca, Levi Lúcio, Vasco Amaral, Roberto Félix, Vasco Sousa) T3B T5D T4B
• (SLE 2010) Featherweight TEX and Parser Correctness (Sebastian Erdweg, Klaus Ostermann) T5D T4C T1A
• (SLE 2011) Formalizing a Domain Specific Language Using SOS: An Industrial Case Study (Frank P. M. Stappers, Sven Weber, Michel Reniers, Suzana Andova, István Nagy) T1C T5D T6B
• (SLE 2011) Semantics First! Rethinking the Language Design Process (Martin Erwig, Eric Walkingshaw) T1A T1C T5D
• (SLE 2012) Termination Analysis for Higher-Order Attribute Grammars (Lijesh Krishnan, Eric Van Wyk) T5D T5B T3A
• (SLE 2012) Temporal Constraint Support for OCL (Bilal Kanso, Safouan Taha) T5D T5C T4A
• (SLE 2012) Guided Merging of Sequence Diagrams (Magdalena Widl, Armin Biere, Petra Kaufmann, Uwe Egly, Marijn J. H. Heule, Gerti Kappel, Martina Seidl, Hans Tompits) T2B T4B T5D
• (SLE 2012) On the Reusable Specification of Non-functional Properties in DSLs (Francisco Durán, Steffen Zschaler, Javier Troya) T1E T3C T5D
• (SLE 2012) Modular Well-Definedness Analysis for Attribute Grammars (Ted Kaminski, Eric Van Wyk) T5B T1D T3A T5D
• (SLE 2012 SI) A survey of grammatical inference in software engineering (Andrew W. Stevenson, James R. Cordy) T5B T2A T5D T3C
• (SLE 2012 SI) Monolithic and modular termination analyses for higher-order attribute grammars (Lijesh Krishnan, Eric Van Wyk) T5B T5D T1D T4A
• (SLE 2012 SI) Specification of temporal properties with OCL (Bilal Kanso, Safouan Taha) T5D T1C T4A T5C
• (SLE 2013) A Model-Driven Approach to Enhance Tool Interoperability Using the Theory of Models of Computation (Papa Issa Diallo, Joël Champeau, Loïc Lagadec) T4B T5D T1D
• (SLE 2013) Whiley: A Platform for Research in Software Verification (David J. Pearce, Lindsay Groves) T5D T1A T1B
• (SLE 2013) A Generic Framework for Symbolic Execution (Andrei Arusoaie, Dorel Lucanu, Vlad Rusu) T5D T1C T4C
• (SLE 2013) Mapping-Aware Megamodeling: Design Patterns and Laws (Zinovy Diskin, Sahar Kokaly, Tom Maibaum) T3A T4B T5D
• (SLE 2013) Partial Instances via Subclassing (Kacper Bąk, Zinovy Diskin, Michał Antkiewicz, Krzysztof Czarnecki, Andrzej Wąsowski) T1A T5D T3A
• (SLE 2013) Towards Controlling Refinements of Statecharts (Conner Hansen, Eugene Syriani, Levi Lúcio) T2B T5D T4C T3C
• (SLE 2014) ProMoBox: A Framework for Generating Domain-Specific Property Languages (Bart Meyers, Romuald Deshayes, Levi Lúcio, Eugene Syriani, Hans Vangheluwe, Manuel Wimmer) T5D T3C T4A T4B
• (SLE 2014) A SAT-Based Debugging Tool for State Machines and Sequence Diagrams (Petra Kaufmann, Martin Kronegger, Andreas Pfandler, Martina Seidl, Magdalena Widl) T5D T4A T1C T5C
• (SLE 2014) Model Checking of CTL-Extended OCL Specifications (Robert Bill, Sebastian Gabmeyer, Petra Kaufmann, Martina Seidl) T5D T1A T4A
• (SLE 2014) Simple, Efficient, Sound and Complete Combinator Parsing for All Context-Free Grammars, Using an Oracle (Tom Ridge) T5B T5F T5D T3A
• (SLE 2014 SI) Symbolic execution based on language transformation (Andrei Arusoaie, Dorel Lucanu, Vlad Rusu) T4C T1C T5D T4A
• (SLE 2014 SI) Intra- and interdiagram consistency checking of behavioral multiview models (Petra Kaufmann, Martin Kronegger, Andreas Pfandler, Martina Seidl, Magdalena Widl) T5D T5B T3C
• (SLE 2015) Managing Uncertainty in Bidirectional Model Transformations (Romina Eramo, Alfonso Pierantonio, Gianni Rosa) T4B T5D T2B T3B
• (SLE 2015) Modular Capture Avoidance for Program Transformations (Nico Ritschel, Sebastian Erdweg) T3B T5D T1D T2B
• (SLE 2015) Designing Languages using Lightning (Loïc Gammaitoni, Pierre Kelsen, Christian Glodt) T4A T5D T1A T1C
• (SLE 2015) A Combined Formal Model for Relational Context-Dependent Roles (Thomas Kühn, Stephan Böhme, Sebastian Götz, Uwe Aßmann) T1A T5D T1B T3C
• (SLE 2015) The Whiley Rewrite Language (WyRL) (David J. Pearce) T3B T4C T4A T5D
• (SLE 2016) Side Effects Take the Blame (Felipe Bañados Schwerter) T1B T1C T4D T5D
• (SLE 2016) Symbolic Execution of High-Level Transformations (Ahmad Salim Al-Sibahi, Aleksandar S. Dimovski, Andrzej Wąsowski) T5D T3B T4C
• (SLE 2017) Engineering Meta-Languages for Specifying Software Languages (Peter D. Mosses) T3A T1C T4A T5D
• (SLE 2017) Ensuring Non-interference of Composable Language Extensions (Ted Kaminski, Eric Van Wyk) T1D T5D T1B T4C
• (SLE 2017) A Formalisation of Parameterised Reference Attribute Grammars (Scott Buckley, Anthony M. Sloane) T3A T5D T1B T1D
• (SLE 2017) Structural Model Subtyping with OCL Constraints (Artur Boronat) T1B T5D T1E T3C
• (SLE 2018) A New Approach for Software Correctness and Reliability (Martin C. Rinard) T5D T4A
• (SLE 2018) Languages as First-Class Citizens (Matteo Cimini) T6D T5D T4D
• (SLE 2018) Messir: A Text-first DSL-based Approach for UML Requirements Engineering (Benoît Ries, Alfredo Capozucca, Nicolas Guelfi) T4A T5D T1D T4C
• (SLE 2018) Deriving Fluent Internal Domain-Specific Languages from Grammars (Arvid Butting, Manuela Dalibor, Gerrit Leonhardt, Bernhard Rumpe, Andreas Wortmann) T3C T4A T5D T4C
• (SLE 2018) Morbig: A Static Parser for POSIX Shell (Yann Régis-Gianas, Nicolas Jeannerod, Ralf Treinen) T1A T4A T5D T5E
• (SLE 2018) A Practical Type System for Safe Aliasing (Dimi Racordon, Didier Buchs) T1B T4A T5D T4D
• (SLE 2018) Analysing Meta-Model Product Lines (Esther Guerra, Juan de Lara, Marsha Chechik, Rick Salay) T1A T5D T2C
• (SLE 2019) A Feature-based Classification of Triple Graph Grammar Variants (Nils B. Weidmann, Robin Oppermann, Patrick Robrecht) T3B T4A T5D T4B
• (SLE 2019) A Vision of Miking: Interactive Programmatic Modeling, Sound Language Composition, and Self-Learning Compilation (David Broman) T3C T4A T5D T1D
• (SLE 2019) The Lands Platform: Lan.guages and D.omain S.yntax (Nick Papoulias) T3C T4A T5D T1D
• (SLE 2019) Empirical Study on the Usage of Graph Query Languages in Open Source Java Projects (Philipp Seifer, Johannes Härtel, Martin Leinberger, Ralf Lämmel, Steffen Staab) T1A T5D T5E
• (SLE 2020) Gradually Typing Strategies (Jeff Smits, Eelco Visser) T1B T4A T5D T4B
• (SLE 2020) A Precedence-Driven Approach for Concurrent Model Synchronization Scenarios using Triple Graph Grammars (Lars Fritsche, Jens Kosiol, Adrian Möller, Andy Schürr, Gabriele Taentzer) T3B T4A T5D T4B
• (SLE 2020) Extrinsically Typed Operational Semantics for Functional Languages (Matteo Cimini, Dale Miller, Jeremy G. Siek) T1B T4A T5D T4C
• (SLE 2020) Featherweight Swift: A Core Calculus for Swift’s Type System (Dimi Racordon, Didier Buchs) T1B T4A T5D T5H
• (SLE 2020) Untangling Mechanized Proofs (Clément Pit-Claudel) T1A T5D T4C T4D
• (SLE 2020) Monadification of Attribute Grammars (Dawn Michaelson, Eric Van Wyk) T1B T4A T5D T5E
• (SLE 2020) A Semantic Framework for PEGs (Sérgio Queiróz de Medeiros, Carlos Olarte) T1C T4A T5D
• (SLE 2021) Automating the Synthesis of Recommender Systems for Modelling Languages (Lissette Almonte, Sara Pérez-Soler, Esther Guerra, Iván Cantador, Juan de Lara) T3C T4A T5D T5E
• (SLE 2021) Executing Certified Model Transformations on Apache Spark (Jolan Philippe, Massimo Tisi, Hélène Coullon, Gerson Sunyé) T3B T4A T5D T5E
• (SLE 2021) Automated Engineering of Metamorphic Testing Environments for Domain-Specific Languages (Pablo C. Cañizares, Pablo Gómez-Abajo, Alberto Núñez, Esther Guerra, Juan de Lara) T3C T4A T5D T5H
• (SLE 2022) Lang-n-Prove: A DSL for Language Proofs (Matteo Cimini) T5D T3A T3C
• (SLE 2022) The Semantics of Plurals (Friedrich Steimann, Marius Freitag) T1C T1A T5D
• (SLE 2022) Property-Based Testing: Climbing the Stairway to Verification (Zilin Chen, Christine Rizkallah, Liam O’Connor, Partha Susarla, Gerwin Klein, Gernot Heiser, Gabriele Keller) T5C T5D T6D
• (SLE 2023) An Executable Semantics for Faster Development of Optimizing Python Compilers (Olivier Melançon, Marc Feeley, Manuel Serrano) T1C T4C T5D
• (SLE 2023) Cross-Level Debugging for Static Analysers (Mats Van Molle, Bram Vandenbogaerde, Coen De Roover) T5D T4A T5H
• (SLE 2024) Type Checking with Rewriting Rules (Dimi Racordon) T1B T5D T3A
• (SLE 2024 SI) Translating meaning representations to behavioural interface specifications (Iat Tou Leong, Raul Barbosa) T5D T4G T2E T5A
• (SLE 2025) Integrating Model Checking into a Live Modeling Environment (Joeri Exelmans, Ciprian Teodorov, Hans Vangheluwe) T5D T4D T4E
• (SLE 2025) Variability Fault Localization by Abstract Interpretation and its Application to SPL Repair (Aleksandar S. Dimovski) T2C T5D T2B
• (SLE 2025) (Semantic) Feature Model Differences with (Q)SAT (Simone Heisinger, Maximilian Heisinger, Martina Seidl) T2C T5D T2B
• (SLE 2026) A Shallow Embedding of Datalog in Lean (Ramy Shahin) T1D T3C T5D

---

The page is maintained by Dr. Vadim Zaytsev a.k.a. @grammarware. Last updated: June 2026.