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?

Creative Commons BY 4.0

Marsha Chechik, Eunsuk Kang, Shahar Maoz, Jan Oliver Ringert, and Allison Sullivan