TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 22451

Principles of Contract Languages

( 06. Nov – 11. Nov, 2022 )

(zum Vergrößern in der Bildmitte klicken)

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/22451

Organisatoren

Kontakt


Programm

Summary

This report documents the program and the outcomes of Dagstuhl Seminar 22451 "Principles of Contract Languages".

Formal, precise analysis of non-trivial software is a task that necessarily must be decomposed. The arguably most important composition principle in programming is the procedure (function, method, routine) call. For this reason, it is natural to decompose the analysis of a program along its call structure. Decomposition in this context means to replace a procedure call with a declarative description, possibly an approximation, of the call's effect. In his seminal work on runtime verification in Eiffel, Bertrand Meyer suggested to use the metaphor of a contract between the user (caller) and implementor (callee) for such a description.

Contracts continue to be a central element in run-time (dynamic) analysis. In the last two decades they also became the dominant decomposition approach in deductive verification and are realized in all major software verification systems. More recently, software contracts are increasingly used in test case generation and model checking. Furthermore, programming languages such as "Racket" or "Dafny" were designed with a notion of contract. Contract-based specification languages are available for mainstream programming languages, notably JML for "Java" and ACSL/ACSL++ for "C"/"C++".

However, there is considerable fragmentation concerning terminology, basic principles, expressivity, and usage of contracts in different research communities. Therefore, this Dagstuhl Seminar convened researchers working with contracts in static verification, runtime verification, as well as testing, with the goal of creating a unified view on software contracts.

The seminar participants discussed the following topics and questions:

  • Sub-procedural contracts: contracts for blocks, loops, suspension points, barriers
  • Combining trace-based specifications for global properties with two-state contracts for recursive procedures
  • Rethink abstract versus implementation-layer specifications
  • Contracts for concurrent languages
  • Contract composition
  • Unify contracts for deductive and runtime verification and testing
  • (Behavioral) types as lightweight contracts
  • Where do contracts come from? Contract synthesis
  • Contract validation, connection to natural language
  • Contracts for refinement (correctness by construction)
  • Contracts for relational properties
  • Debugging contracts
  • Domain-specific contract languages
Copyright Dilian Gurov, Reiner Hähnle, Marieke Huisman, and Giles Reger

Motivation

Formal, precise analysis of non-trivial software is a task that necessarily must be decomposed. The arguably most important composition principle in programming is the procedure (function, method, routine) call. For this reason, it is natural to decompose the analysis of a program along its call structure. Decomposition in this context means to replace a procedure call with a declarative description, possibly an approximation, of the call's effect. In his seminal work on runtime verification in Eiffel, Bertrand Meyer suggested to use the metaphor of a contract between the user (caller) and implementor (callee) for such a description.

Contracts continue to be a central element in run-time (dynamic) analysis. In the last two decades they also became the dominant decomposition approach in deductive verification and are realized in all major software verification systems. More recently, software contracts are increasingly used in test case generation and model checking. Furthermore, programming languages such as "Racket" were designed with a notion of contract. Contract-based specification languages are available for mainstream programming languages, notably JML for "Java" and ACSL/ACSL++ for "C"/"C++".

However, there is considerable fragmentation concerning terminology, basic principles, expressivity, and usage of contracts in different research communities. Therefore, this Dagstuhl Seminar aims to convene researchers working with contracts in static verification, runtime verification, as well as testing, with the goal of creating a unified view on software contracts.

The seminar will address the following topics and questions:

  • What are the fundamental aspects of contracts for software development?
  • What format or structure should contracts have?
  • How expressive does a contract language need to be?
  • How do contract formats depend on their use cases?
  • How should contracts be composed and decomposed?
  • How can contracts be used for documentation, testing and verification?
  • How can a unified view on contracts help integrating static and dynamic techniques?
  • How can contracts support agile software development?
  • How should contracts be refined upon a failed verification attempt?

The format of the seminar will be as follows. Each day will be dedicated to a specific topic and will consist, in the morning, of one or two tutorials that make a general overview of the topic, followed by short technical talks. During the afternoon, we will have brief pitches from participants to spark off discussions in groups on important questions raised in the morning. The day will be wrapped up by a plenary discussion in which the groups will present a summary of their findings.

Copyright Dilian Gurov, Reiner Hähnle, Marieke Huisman, and Giles Reger

Teilnehmer
  • Wolfgang Ahrendt (Chalmers University of Technology - Göteborg, SE) [dblp]
  • Bernhard Beckert (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Alessandro Cimatti (Bruno Kessler Foundation - Trento, IT) [dblp]
  • David Cok (Safer Software Consulting - Rochester, US) [dblp]
  • Claire Dross (AdaCore - Paris, FR)
  • Gidon Ernst (LMU München, DE) [dblp]
  • Dilian Gurov (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
  • Reiner Hähnle (TU Darmstadt, DE) [dblp]
  • Sylvain Hallé (University of Quebec at Chicoutimi, CA) [dblp]
  • Paula Herber (Universität Münster, DE) [dblp]
  • Asmae Heydari Tabar (TU Darmstadt, DE) [dblp]
  • Marieke Huisman (University of Twente - Enschede, NL) [dblp]
  • Marie-Christine Jakobs (TU Darmstadt, DE) [dblp]
  • Eduard Kamburjan (University of Oslo, NO) [dblp]
  • Nikolai Kosmatov (Thales Research & Technology - Palaiseau, FR) [dblp]
  • Srdan Krstic (ETH Zürich, CH) [dblp]
  • Sophie Lathouwers (University of Twente - Enschede, NL) [dblp]
  • Martin Leucker (Universität Lübeck, DE) [dblp]
  • Christian Lidström (KTH Royal Institute of Technology - Stockholm, SE) [dblp]
  • Rosemary Monahan (National University of Ireland - Maynooth, IE) [dblp]
  • Doron A. Peled (Bar-Ilan University - Ramat Gan, IL) [dblp]
  • Giles Reger (University of Manchester, GB) [dblp]
  • Kristin Yvonne Rozier (Iowa State University - Ames, US) [dblp]
  • Philipp Rümmer (Uppsala University, SE) [dblp]
  • Thomas Santen (Formal Assurance - Aachen, DE) [dblp]
  • Marco Scaletta (TU Darmstadt, DE)
  • Ina Schaefer (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Julien Signoles (CEA LIST - Gif-sur-Yvette, FR) [dblp]
  • Alexander J. Summers (University of British Columbia - Vancouver, CA) [dblp]
  • Mattias Ulbrich (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Petra van den Bos (University of Twente - Enschede, NL)

Klassifikation
  • Logic in Computer Science
  • Programming Languages
  • Software Engineering

Schlagworte
  • semantics
  • formal methods
  • software engineering
  • verification
  • logic