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 12461

Games and Decisions for Rigorous Systems Engineering

( 11. Nov – 16. Nov, 2012 )


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

Organisatoren

Kontakt


Programm

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).


Teilnehmer
  • 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]

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

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