Dagstuhl Seminar 25392
Specification Engineering: Foundations for the Future of Software Development
( Sep 21 – Sep 26, 2025 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/25392
Organizers
- Marsha Chechik (University of Toronto, CA)
- Eunsuk Kang (Carnegie Mellon University - Pittsburgh, US)
- Shahar Maoz (Tel Aviv University, IL)
- Jan Oliver Ringert (Bauhaus-Universität Weimar, DE)
- Allison Sullivan (University of Texas at Arlington, US)
Contact
- Michael Gerke (for scientific matters)
- Jutka Gasiorowski (for administrative matters)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
Formal specifications are mathematically precise descriptions of the behavior or properties of a system. Specifications are an essential component in a variety of tasks in software engineering, including software verification, testing, modeling, requirements engineering, and program synthesis. Despite a wealth of research on techniques and tools that take specifications as input, relatively less has been explored on addressing the challenges of coming up with specifications in the first place, and maintaining them as system requirements evolve. Typically, specifications are assumed to have been created by software engineers, who may not have sufficient training or expertise in specification languages. Little is understood about what makes a specification “correct” or “high-quality”, and how to validate specifications to ensure that they accurately reflect a user’s intent. Specification tools are also notorious for their poor usability and high learning curve.
While producing quality specifications has been a longstanding problem, recent advances in AI technologies, such as large-language models (LLMs), make it a timely problem to address from new perspectives. Automatically generating code from a high-level specification will likely emerge as a dominant paradigm for software development in the future. Thus, being able to write, maintain and evolve high-quality specifications – the process of specification engineering – will become an essential skill for software engineers. LLMs are also being explored by researchers as a promising way of generating formal specifications from natural language requirements. However, since LLMs themselves do not provide guarantees about the correctness or quality of their output, new methods for validating and improving the quality of generated specifications will be crucial to make them reliable and useful.
This Dagstuhl Seminar “Specification Engineering: Foundations for the Future of Software Development” (25392) brought together leading researchers in software engineering and formal methods to identify foundational problems and build a roadmap for specification engineering as a central activity in future development processes. The seminar was organized around the following questions:
- Quality and Validation: What are key properties of a high-quality specification? How do we debug, validate, and repair specifications for these properties?
- Usability: How do we make it easier for engineers to express and validate their intent in a specification language? How do we make specifications readable and comprehensible?
- Scalable Specification Construction: How do we construct large, complex specifications out of smaller ones? How do we facilitate reuse of specifications? How do we support incremental, modular changes to a specification?
- Specification for/with AI: How do we use and tailor AI-based tools for specification-driven tasks such as code generation and verification? How do we make these models more effective at generating specifications from natural languages?
Activities
The seminar consisted of (1) several invited, “anchoring” talks around the four major topics listed above, (2) a series of shorter, “lightning” talks where participants shared new ideas, open problems, or ongoing projects on the topic of specification, and (3) two sets of breakout discussions. The first set of breakouts was assigned based on the four topics; after the initial discussions, the participants were encouraged to suggest or form different groups based on their topics of interest that emerged. The resulting second set of breakouts were centered around the topic of AI, covering LLMs for specification activities, specification of LLMs, and the use of AI for domain modeling. These activities were interleaved with ad-hoc discussions around the very concept of “specification” itself as well as planning for post-seminar activities and collaborations.
Outcome
Among many stimulating discussions around the topic of specification, two major themes emerged. First, the participants realized that the very idea of “specification” may not be as well-defined or agreed upon as many had previously thought before the seminar. For example, to some participants, a specification had a specific meaning as a type of artifact that describes the expected behavior of a program or a system (e.g., API contracts), while others thought that nearly every software artifact (e.g., code) could be considered a specification. After a seminar-wide discussion, the participants agreed that it would be more meaningful to talk about properties of a specification (e.g., whether it is formal or informal, readable, analyzable, modifiable, for what purpose it is used, etc.,) rather than attempting to define what a specification is (and is not).
Second, many participants agreed that specifications will have an essential role in the age of AI-driven development and provide new opportunities for research as well as engagement with practitioners. For example, natural language prompts are emerging as a common mechanism to specify developers’ intent and system requirements, from which an implementation is automatically generated. However, it was also noted that informal, unstructured prompts are not an ideal specification mechanism for developing, debugging, and maintaining complex software systems, and that more structured specification methods are needed to support both developers and AI agents in these tasks. On the other hand, the participants also agreed that traditional specification methods and tools developed by the research community will likely need to be adapted or rethought to support the fuzzy, interactive, and informal ways in which developers collaborate with AI to develop software.
Creative Commons BY 4.0
Marsha Chechik, Eunsuk Kang, Shahar Maoz, Jan Oliver Ringert, and Allison Sullivan
Formal specifications are mathematically precise descriptions of the behavior or properties of a system. Specifications are an essential component in a variety of tasks in software engineering, including software verification, testing, modeling, requirements engineering, and program synthesis. Despite a wealth of research on techniques and tools that take specifications as an input, relatively less has been explored on addressing the challenges of coming up with specifications in the first place, and maintaining them as system requirements evolve. Typically, specifications are assumed to have been created by software engineers, who may not have sufficient training or expertise in specification languages. Little is understood about what makes a specification “correct” or “high-quality”, and how to validate specifications to ensure that they accurately reflect a user’s intent. Specification tools are also notorious for their poor usability and high learning curve.
While producing quality specifications has been a longstanding problem, recent advances in AI technologies, such as large-language models (LLMs), make it a timely problem to address from new perspectives. Automatically generating code from a high-level specification will likely emerge as a dominant paradigm for software development in the future. Thus, being able to write, maintain and evolve high quality specifications — the process of specification engineering — will become an essential skill for software engineers. LLMs are also being explored by researchers as a promising way of generating formal specifications from natural language requirements. However, since LLMs themselves do not provide guarantees about the correctness or quality of their output, new methods for validating and improving the quality of generated specifications will be crucial to make them reliable and useful.
This Dagstuhl Seminar aims to bring together leading researchers in software engineering and formal methods to identify foundational problems and build a roadmap for specification engineering as a central activity in future development processes. The seminar will be centered around the following questions:
(1) Quality & Validation: What are key properties of a high-quality specification? How do we debug, validate, and repair specifications for these properties?
(2) Usability: How do we make it easier for engineers to express and validate their intent in a specification language? How do we make specifications readable and comprehensible?
(3) Scalable Specification Construction: How do we construct large, complex specifications out of smaller ones? How do we facilitate reuse of specifications? How do we support incremental, modular changes to a specification?
(4) Specification for/with AI: How do we use and tailor AI-based tools for specification-driven tasks such as code generation and verification? How do we make these models more effective at generating specifications from natural languages?
Marsha Chechik, Eunsuk Kang, Shahar Maoz, Jan Oliver Ringert, and Allison Sullivan
Please log in to DOOR to see more details.
- Thorsten Berger (Ruhr-Universität Bochum, DE) [dblp]
- José Creissac Campos (University of Minho, PT) [dblp]
- Mauricio Castillo-Effen (Lockheed Systems - Arlington, US) [dblp]
- Marsha Chechik (University of Toronto, CA) [dblp]
- Benoit Combemale (INRIA - Rennes, FR) [dblp]
- Alcino Cunha (University of Minho, PT) [dblp]
- Jyotirmoy Deshmukh (USC - Los Angeles, US) [dblp]
- Matthew Dwyer (University of Virginia - Charlottesville, US) [dblp]
- Lars Grunske (HU Berlin, DE) [dblp]
- Reiner Hähnle (TU Darmstadt, DE) [dblp]
- Taylor T. Johnson (Vanderbilt University - Nashville, US) [dblp]
- Eunsuk Kang (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Ekaterina Komendantskaya (Heriot-Watt University - Edinburgh, GB) [dblp]
- Yi Li (Nanyang TU - Singapore, SG) [dblp]
- Shahar Maoz (Tel Aviv University, IL) [dblp]
- Rômulo Meira-Góes (Pennsylvania State University - University Park, US) [dblp]
- Alexandra Mendes (University of Porto, PT) [dblp]
- Federico Mora (University of Waterloo, CA)
- Daniel Neider (TU Dortmund, DE) [dblp]
- Phillippe Palanque (Toulouse University, FR) [dblp]
- Jan Oliver Ringert (Bauhaus-Universität Weimar, DE) [dblp]
- Bernhard Rumpe (RWTH Aachen, DE) [dblp]
- Kathryn T. Stolee (North Carolina State University - Raleigh, US) [dblp]
- Allison Sullivan (University of Texas at Arlington, US) [dblp]
- Harold Thimbleby (Swansea University, GB) [dblp]
- Michael W. Whalen (Amazon Inc. - Minneapolis, USA & The University of Minnesota - Minneapolis, USA) [dblp]
- Pamela Zave (Princeton University, US) [dblp]
Classification
- Software Engineering
Keywords
- Software specification
- Specification engineering
- Software assurance
- Formal methods
