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 14442

Symbolic Execution and Constraint Solving

( 27. Oct – 30. Oct, 2014 )

(zum Vergrößern in der Bildmitte klicken)

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

Organisatoren

Koordinator
  • Raimondas Sasnauskas (University of Utah - Salt Lake City, US)

Kontakt

Gemeinsame Dokumente


Motivation

Symbolic execution has garnered a lot of attention in recent years as an effective technique for generating high-coverage test suites, finding deep errors in complex software applications, and more generally as one of the few techniques that is useful across the board in myriad software engineering applications. While key ideas behind symbolic execution were introduced more than three decades ago, it was only recently that these techniques became practical as a result of significant advances in constraint satisfiability and scalable combinations of concrete and symbolic execution. The result has been an explosion in applications of symbolic execution techniques in software engineering, security, formal methods and systems research. Furthermore, researchers are combining symbolic execution with traditional program analysis techniques in novel ways to address longstanding software engineering problems. This in turn has led to rapid developments in both constraint solvers and symbolic execution techniques, necessitating an in-depth exchange of ideas between researchers working on solvers and symbolic techniques, best accomplished through dedicated workshops. Hence, the goal of this seminar is to bring together the leading researchers in the fields of symbolic execution and constraint solving, foster greater communication, exchange ideas about new research directions and feedback from solver users to developers. In the following, we highlight the main challenges in modern symbolic execution techniques and constraint solving that will be addressed during the seminar from different research perspectives:

  • How to cope with path explosion?
  • How to exploit the type of constraints generated during the symbolic execution of real programs?
  • How to design and implement solvers that can handle rich constraints generated through symbolic execution and program analysis?
  • How to enable precise analysis of program statements?
  • How to extend symbolic execution to efficiently handle concurrent programs?

Symbolic execution plays a key role in the work on several different communities - particularly software engineering, testing, verification, computer systems and software security - as evidenced by the large number of publications on this topic in top venues in each of these areas, such as ICSE, FSE, ASE (software engineering); OSDI, EuroSys, ICDCS, IPSN, ASPLOS (systems); ISSTA, ICST (testing); CAV, HVC (verification); and CCS, IEEE Security and Privacy (security). One of the core goals of the seminar is to bring together these many different communities that work on symbolic execution techniques, communities which unfortunately rarely talk to each other. We believe that the exchange of ideas between these different communities - each with their own methods and perspectives on the field - would help accelerate the future development of symbolic execution and constraint solving techniques. In terms of concrete outcomes, we believe the seminar is likely to lead to several collaboration projects both between members of the same community, but also between members of different communities that work on the same problems in the symbolic execution and constraint solving areas.


Executive Summary

Symbolic execution has garnered a lot of attention in recent years as an effective technique for generating high-coverage test suites, finding deep errors in complex software applications, and more generally as one of the few techniques that is useful across the board in myriad software engineering applications. While key ideas behind symbolic execution were introduced more than three decades ago, it was only recently that these techniques became practical as a result of significant advances in constraint satisfiability and scalable combinations of concrete and symbolic execution. The result has been an explosion in applications of symbolic execution techniques in software engineering, security, formal methods and systems research. Furthermore, researchers are combining symbolic execution with traditional program analysis techniques in novel ways to address longstanding software engineering problems. This in turn has led to rapid developments in both constraint solvers and symbolic execution techniques, necessitating an in-depth exchange of ideas between researchers working on solvers and symbolic techniques, best accomplished through dedicated workshops.

Hence, one of the main goals of this Dagstuhl seminar was to bring together leading researchers in the fields of symbolic execution and constraint solving, foster greater communication between these two communities and discuss new research directions in these fields. The seminar had 34 participants from Canada, France, Germany, Norway, Singapore, South Africa, Spain, Switzerland, The Netherlands, United Kingdom and United States, from both academia, research laboratories, and the industry. More importantly, the participants represented several different communities, with the topics of the talks and discussions reflecting these diverse interests: testing, verification, security, floating point constraint solving, hybrid string-numeric constraints, debugging and repair, education, and commercialization, among many others.


Teilnehmer
  • Sébastien Bardin (CEA LIST, FR) [dblp]
  • Earl T. Barr (University College London, GB) [dblp]
  • Cristian Cadar (Imperial College London, GB) [dblp]
  • Satish Chandra (Samsung Electronics - San Jose, US) [dblp]
  • Maria Christakis (ETH Zürich, CH) [dblp]
  • Peter Collingbourne (Google Inc. - Mountain View, US) [dblp]
  • Jorge R. Cuéllar (Siemens AG - München, DE) [dblp]
  • Morgan Deters (New York University, US) [dblp]
  • Alastair F. Donaldson (Imperial College London, GB) [dblp]
  • Juan Pablo Galeotti (Universität des Saarlandes, DE) [dblp]
  • Vijay Ganesh (University of Waterloo, CA) [dblp]
  • Indradeep Ghosh (Fujitsu Labs of America Inc. - Sunnyvale, US) [dblp]
  • Arnaud Gotlieb (Simula Research Laboratory - Lysaker, NO) [dblp]
  • Istvan Haller (VU University Amsterdam, NL) [dblp]
  • Wei Le (Iowa State University - Ames, US) [dblp]
  • Paul Marinescu (Imperial College London, GB) [dblp]
  • Benjamin Mehne (University of California - Berkeley, US)
  • Martin Ochoa (TU München, DE) [dblp]
  • Albert Oliveras (Polytechnic University of Catalonia, ES) [dblp]
  • Hristina Palikareva (Imperial College London, GB) [dblp]
  • Ruzica Piskac (Yale University, US) [dblp]
  • John Regehr (University of Utah - Salt Lake City, US) [dblp]
  • Abhik Roychoudhury (National University of Singapore, SG) [dblp]
  • Neha Rungta (NASA - Moffett Field, US) [dblp]
  • Raimondas Sasnauskas (University of Utah - Salt Lake City, US) [dblp]
  • Koushik Sen (University of California - Berkeley, US) [dblp]
  • Laurent Simon (University of Bordeaux, FR) [dblp]
  • Oscar Soria Dustmann (RWTH Aachen, DE) [dblp]
  • Nikolai Tillmann (Microsoft Corporation - Redmond, US) [dblp]
  • Willem Visser (Stellenbosch University - Matieland, ZA) [dblp]
  • Klaus Wehrle (RWTH Aachen, DE) [dblp]
  • Nicky Williams (CEA, FR) [dblp]
  • Christoph M. Wintersteiger (Microsoft Research UK - Cambridge, GB) [dblp]
  • Lingming Zhang (University of Texas at Dallas, US) [dblp]

Verwandte Seminare
  • Dagstuhl-Seminar 19062: Bringing CP, SAT and SMT together: Next Challenges in Constraint Solving (2019-02-03 - 2019-02-06) (Details)
  • Dagstuhl-Seminar 22291: Machine Learning and Logical Reasoning: The New Frontier (2022-07-17 - 2022-07-22) (Details)

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

Schlagworte
  • Symbolic Execution
  • Software Testing
  • Automated Program Analysis
  • Constraint Solvers