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 14442

Symbolic Execution and Constraint Solving

( Oct 27 – Oct 30, 2014 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/14442

Organizers

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

Contact

Shared Documents


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.


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

Related Seminars
  • 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)

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

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