Dagstuhl Seminar 12511
Divide and Conquer: the Quest for Compositional Design and Analysis
( Dec 16 – Dec 21, 2012 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/12511
Organizers
- Marieke Huisman (University of Twente, NL)
- Barbara Jobstmann (VERIMAG - Grenoble, FR)
- Ina Schaefer (TU Braunschweig, DE)
- Marielle Stoelinga (University of Twente, NL)
Contact
Compositionality is a key concept in computer science: only by breaking down a large system into smaller pieces, we can build today's complex software and hardware systems. The same holds true for verification and analysis: realistic systems can only be analyzed by chopping them up into smaller parts. Thus, compositionality has been widely studied in various different settings, and by different communities: people in programming languages, software verification, and model checking have all come up with their own techniques and solutions.
Thus, the goal of this workshop has been to bring together these fields and communities, so that they can learn from and cross-fertilize each other. We have succeeded in doing so: through three extensive tutorials, longer and shorter presentations, and working sessions, researchers from different areas have learned about each others problems, techniques, and approaches.
The scientific programme was built around four corners stones
- Personal introductions.
- Three well-received tutorials:
- Compositional programming by Oscar Nierstrasz
- Compositional verification by Arnd Poetzsch-Heffter
- Compositional modelling by Arend Rensink
- Regular presentations, presenting in-depth technical knowlegde on:
- Verification of programming languages
- Automatic synthesis
- Interface theories
- Model checking
- Contract-based design
- Software product lines
- Working group sessions:
- Working group on software product lines
- Working group on Benchmark for Industrial Verification/Synthesis Problems
- Working group on Modular Full Functional Specification and Verification of C and Java programs that Perform I/O
- Model checking vd deducutive verification
- Compositional Synthesis of Reactive Systems
- Wolfgang Ahrendt (Chalmers UT - Göteborg, SE) [dblp]
- Simon Bliudze (EPFL - Lausanne, CH) [dblp]
- Ferruccio Damiani (University of Turin, IT)
- Rayna Dimitrova (Universität des Saarlandes, DE) [dblp]
- Christian Eisentraut (Universität des Saarlandes, DE)
- Bernd Finkbeiner (Universität des Saarlandes, DE) [dblp]
- Kathi Fisler (Worcester Polytechnic Institute, US) [dblp]
- Susanne Graf (VERIMAG - Grenoble, FR)
- Dilian Gurov (KTH Royal Institute of Technology, SE) [dblp]
- Reiner Hähnle (TU Darmstadt, DE) [dblp]
- Ludovic Henrio (INRIA Sophia Antipolis - Méditerranée, FR)
- Marieke Huisman (University of Twente, NL) [dblp]
- Bart Jacobs (KU Leuven, BE) [dblp]
- Barbara Jobstmann (VERIMAG - Grenoble, FR) [dblp]
- Einar Broch Johnsen (University of Oslo, NO) [dblp]
- Christian Kästner (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Shmuel Katz (Technion - Haifa, IL)
- Shriram Krishnamurthi (Brown University - Providence, US) [dblp]
- Malte Lochau (TU Darmstadt, DE) [dblp]
- Oscar M. Nierstrasz (Universität Bern, CH) [dblp]
- Doron A. Peled (Bar-Ilan University - Ramat Gan, IL) [dblp]
- Arnd Poetzsch-Heffter (TU Kaiserslautern, DE) [dblp]
- Erik Poll (Radboud University Nijmegen, NL) [dblp]
- Sophie Quinton (TU Braunschweig, DE) [dblp]
- Johannes Reich (SAP SE - Walldorf, DE)
- Arend Rensink (University of Twente, NL) [dblp]
- Ina Schaefer (TU Braunschweig, DE) [dblp]
- Malte Schwerhoff (ETH Zürich, CH)
- Vasiliki Sfyrla (VISEO - Lyon, FR)
- Marjan Sirjani (Reykjavik University, IS) [dblp]
- Lei Song (Universität des Saarlandes, DE)
- Martin Steffen (University of Oslo, NO)
- Marielle Stoelinga (University of Twente, NL) [dblp]
- Ufuk Topcu (University of Pennsylvania, US) [dblp]
- Stavros Tripakis (University of California - Berkeley, US) [dblp]
- Andrzej Wasowski (IT University of Copenhagen, DK) [dblp]
Classification
- semantics / formal methods
- software engineering
- verification / logic
Keywords
- Compositionality
- Modeling
- Verification
- Synthesis
- Components
- Interface
- Service-Oriented Architectures
- Software Product Lines
