TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 12461

Games and Decisions for Rigorous Systems Engineering

( Nov 11 – Nov 16, 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/12461

Organizers

Contact


Schedule

Summary

Principled approaches to systems design offer several advantages, including developing safety-critical systems and scaling technological advances with multi-core processes and cloud computing. Rigorous mathematical techniques, such as model checking, decision procedures, and abstract interpretation, are dominantly used a posteriori in systems engineering: a program is formally analyzed after it has been developed. In the context of rigorous systems engineering, post-hoc verification is however very costly and error-prone. The explosion of concurrent computation in the new generation of embedded systems has therefore motivated the integration of established methods with novel techniques in the design process from day one.

Such an integration has been materialized in using game theoretic synthesis of reactive systems from higher level design requirements. In many synthesis algorithms, it is better to work with symbolic representations, where the state space is modeled using logical formulas. This enables techniques to scale to potentially infinite models, but requires decision procedures for checking the validity of sentences in the pertinent logical theories. The increasingly complex integration of model checking with complementary techniques such as software testing has imposed new requirements on decision procedures, such as proof generation, unsatisfiable core extraction, and interpolation.

The main goal of the Dagstuhl Seminar 12461 "Games and Decisions for Rigorous Systems Engineering" was to bring together researchers working in the field of rigorous systems engineering, the tool-supported application of mathematical reasoning principles to the design and verification of complex software and hardware systems. The seminar had a special focus on developing systems (reactive, concurrent, distributed) using recent advances in game theoretic synthesis and in decision procedures and automated deduction techniques.

The seminar covered the following three main areas:

  • software verification (reactive, concurrent, distributed);
  • game theory and reactive synthesis;
  • decision procedures (SAT, SMT, QBF) and theorem proving (first and higher order).

Within the scope of these areas, the seminar addressed tooling around software testing, model checking, interpolation, decision procedures, and model finding methods in automated theorem proving.

In the spirit of advancing tools and theory in related areas of theorem proving and model checking, the seminar schedule included tutorials on games, synthesis, theorem proving; research talks on recent results; and discussion sessions on applications and exchange formats for benchmarking tools.

The seminar fell on 5 days in the week of November 12-16, 2012. All together, 43 researchers participated (11 women and 32 men).


Participants
  • Francesco Alberti (University of Lugano, CH)
  • Dirk Beyer (Universität Passau, DE) [dblp]
  • Nikolaj S. Bjørner (Microsoft Corporation - Redmond, US) [dblp]
  • Tomáš Brázdil (Masaryk University - Brno, CZ) [dblp]
  • Krishnendu Chatterjee (IST Austria - Klosterneuburg, AT) [dblp]
  • Swarat Chaudhuri (Rice University - Houston, US) [dblp]
  • Laurent Doyen (ENS - Cachan, FR) [dblp]
  • Uwe Egly (TU Wien, AT) [dblp]
  • Azadeh Farzan (University of Toronto, CA) [dblp]
  • Bernd Finkbeiner (Universität des Saarlandes, DE) [dblp]
  • Alberto Griggio (Bruno Kessler Foundation - Trento, IT) [dblp]
  • Aarti Gupta (NEC Laboratories America, Inc. - Princeton, US) [dblp]
  • Ashutosh Kumar Gupta (IST Austria - Klosterneuburg, AT)
  • Arie Gurfinkel (Carnegie Mellon University - Pittsburgh, US) [dblp]
  • Jochen Hoenicke (Universität Freiburg, DE)
  • Radu Iosif (VERIMAG - Grenoble, FR) [dblp]
  • Moa Johansson (Chalmers UT - Göteborg, SE) [dblp]
  • Igor Konnov (TU Wien, AT) [dblp]
  • Konstantin Korovin (University of Manchester, GB) [dblp]
  • Laura Kovács (TU Wien, AT) [dblp]
  • Axel Legay (INRIA Rennes - Bretagne Atlantique, FR) [dblp]
  • Rupak Majumdar (MPI-SWS - Kaiserslautern, DE) [dblp]
  • Anca Muscholl (University of Bordeaux, FR) [dblp]
  • Albert Oliveras (Polytechnic University of Catalonia, ES) [dblp]
  • Joel Ouaknine (University of Oxford, GB) [dblp]
  • David Parker (University of Birmingham, GB) [dblp]
  • Brigitte Pientka (McGill University - Montreal, CA) [dblp]
  • Ruzica Piskac (MPI-SWS - Saarbrücken, DE) [dblp]
  • Albert Rubio (UPC - Barcelona, ES) [dblp]
  • Andrey Rybalchenko (TU München, DE) [dblp]
  • Helmut Seidl (TU München, DE) [dblp]
  • Martina Seidl (Universität Linz, AT) [dblp]
  • Natasha Sharygina (University of Lugano, CH) [dblp]
  • Ana Sokolova (Universität Salzburg, AT) [dblp]
  • Armando Solar-Lezama (MIT - Cambridge, US) [dblp]
  • Eugenia Ternovska (Simon Fraser University - Burnaby, CA) [dblp]
  • Helmut Veith (TU Wien, AT) [dblp]
  • Tomas Vojnar (Brno University of Technology, CZ) [dblp]
  • Andrei Voronkov (University of Manchester, GB) [dblp]
  • Georg Weissenbacher (TU Wien, AT) [dblp]
  • Josef Widder (TU Wien, AT) [dblp]
  • Thomas Wies (New York University, US) [dblp]
  • Florian Zuleger (TU Wien, AT) [dblp]

Classification
  • semantics / formal methods
  • software engineering
  • verification / logic

Keywords
  • Systems Engineering
  • Software Verification
  • Reactive Synthesis
  • Automated Deduction