Tracks

1) Rigorous Engineering of Collective Adaptive Systems

Organizers:

Rocco de Nicola

Stefan Jähnichen

Martin Wirsing

2) Documentation as First Class Citizen

Organizers:

Bernhard Steffen

Klaus Havelund

3) X-by-Construction Meets Runtime Verification

Organizers:

Maurice ter Beek

Loek Cleophas

Martin Leucker 

Ina Schaefer

4) Automated Software Re-Engineering

Organizers:

Serge Demeyer

Reiner Hähnle

Heiko Mantel

5) Digital Twin Engineering

Organizers:

John Fitzgerald

Tiziana Margaria

Peter Gorm Larsen

Jim Woodcock

6) Specify This – Bridging gaps between program specification paradigms

Organizers:
Wolfgang Ahrendt, Chalmers University of Technology, SE
Marieke Huisman, University of Twente, NL
Mattias Ulbrich, Karlsruhe Institute of Technology, DE
Paula Herber, University of Münster, DE

Specify This – Bridging gaps between program specification paradigms

The field of program verification has seen considerable successes in recent years. At the same
time, both the variety of properties that can be specified and the collection of approaches that
solve such program verification challenges have specialised and diversified a lot. Examples
include contract-based deductive specification and verification of functional properties, the
specification and verification of temporal properties using model checking or static analyses for
secure information flow properties. While this diversification enables the formal analyses of
properties that were not accessible a few years ago, it may leave the impression of isolated
solutions that solve different isolated problems.

Here lies a great potential that waits to be uncovered: If an approach can be extended to be
able to interpret specifications used in other approaches and to use them beneficially in its
analyses, a considerable extension of the power and reach of formal analyses is achievable. A
discipline of “separation of concerns” can be obtained, by, e.g., combining temporal
specifications of a protocol implementation with a contract-based specification of its
implementation.

Within this track, we will investigate and discuss what can be achieved in joint efforts of the
communities of different specification and verification techniques, including dynamic (XXX?) and
static analysis, model checking, deductive verification, security analyses, testing. This track is a
natural next step following a series of well-structured online discussions within the VerifyThis
community during the last year. There, we identified first candidates for the
combination/interplay of formal program verification methods. During ISoLA 2022, we will
address questions such as how specifications which are shared between different approaches
should look like, how different abstraction levels can be bridged, how semantical differences can
be resolved, which application areas can benefit from which method combinations, what
artifacts can be carried forward through different verification technologies, what role user
interaction (in form of specifications) plays, and how can we integrate the various techniques
into the software, and hybrid/cyber-physical system development processes.

Potential attendants:
– Dilian Gurov
– Gidon Ernst
– Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich
– David Cok, Gary Leavens
– Gerardo Schneider
– Thomas Santen
– Jaco van de Pol
– The track organisers

7) Verification and Validation of Concurrent and Distributed Heterogeneous Systems

Organizers:

Marieke Huismann

Cristina Seceleanu

8) Verification Meets Machine Learning

Organizers:

Kim Larsen

Axel legay

Bernhard Steffen

Marielle Stoelinga

Doctoral Symposium

Organizers

Anna-Lena Lamprecht

Falk Howar

 

Industrial Day

Falk Howar

Axel Hessenkämper

Andreas Rausch

Hardi Hungar

Rigorous Examination of Reactive Systems (RERS)