- Sasa Misailovic (MIT - Cambridge, US)
- Annette Beyer (for administrative matters)
Dagstuhl Seminar Wiki
- Dagstuhl Seminar Wiki (Use personal credentials as created in DOOR to log in)
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Computing has entered the era of approximation, in which hardware and software operate on and reason about estimates. For example, a navigation application turns maps and location estimates from hardware GPS sensors into driving directions; a speech recognition application turns an analog signal into a likely sentence; search turns queries into information; network protocols deliver unreliable messages; and recent research shows promise that approximate hardware and software can profitably trade result quality for energy efficiency. Millions of people already use software that computes with and reasons approximate/probabilistic data daily. These complex systems require sophisticated algorithms to deliver accurate answers quickly, at scale, and with energy efficiency, and approximation is often the only way to meet these competing goals.
Despite their ubiquity, economic significance, and societal impact, building such applications is difficult and requires not only expertise across the system stack, but also expertise in statistics and application-specific domain knowledge. Non-expert developers need tools and expertise to help them design, code, and verify these complex systems.
Several research communities are independently investigating methodologies and techniques to model, analyze, and manage uncertainty in and throughout software systems.
Probabilistic model checking is widely used to support the design and analysis of computer systems, and has been rapidly gaining in importance in recent years. Traditionally, models such as Markov chains have been used to analyze system performance, where typically queuing theory is applied to obtain quantitative characteristics. Probabilistic modeling is also needed to quantify unreliable or unpredictable behavior, for example in fault-tolerant systems and communication protocols, where properties such as component failure and packet loss can be described probabilistically.
However, the applications of probabilistic model checking to software engineering is at the current stage mostly limited to early phases of development, where design models are translated in a more or less automatic way to corresponding stochastic models. Nonetheless, design models are hard to keep consistent with implementation, where code artifacts are in general only partially compliant with their intended design. Quantitative software analysis aims at bringing the verification of probabilistic concerns at code level, designing procedures operating directly on code artifacts. This extends the scope of probabilistic analysis to later stages of development processes, potentially supporting also wide spreading agile methods whose core artifacts are often code.
While quantitative program analysis is focused on general programs dealing with probabilistic phenomena (e.g., unpredictable interaction with users), probabilistic programming makes uncertainty a first-class concept and thus enables probabilistic inference. Probabilistic programming languages augment existing programming languages with probabilistic primitives. The major goal of these languages is the efficient implementation of probabilistic inference, which combines a model (written in the probabilistic programming language) with observed evidence to infer a distribution over variables in the program in light of that evidence. These languages abstract the details of inference, and so see frequent use by machine learning experts when building their models, as well as professionals required to model physical, social, and economic phenomena requiring an explicit account for uncertainty while elaborating computational models.
To tackle the challenge of uncertainty through the whole stack of complex computing systems, approximate computing is an emerging research area that focuses on devising systematic approaches for automating development of approximate software that runs on today's commodity and approximate hardware, or tomorrow's more exotic approximate hardware. The goal of approximate computing is to empower a developer with the understanding of how approximate hardware and software affect the application's accuracy results and to automate the management of accuracy, energy consumption, and performance. To achieve this goal, approximate computing is by nature a multidisciplinary field bringing together researchers from software systems - programming languages and software engineering - and hardware systems - circuit design and hardware architecture.
The aim of this seminar is to bring together academic and industrial researchers from the areas of probabilistic model checking, quantitative software analysis, probabilistic programming, and approximate computing to share their recent progresses, identify the main challenges, and foster collaborations on common interests and problems.
Uncertainty and approximation are becoming first class concepts in software design and development. Many application domains, including biology, multimedia processing, finance, engineering, and social sciences, need software to formalize and study intrinsically uncertain phenomena. Furthermore, the ubiquity of software, especially driven by the Internet and mobility - such as driving applications that estimate routes, speech processing applications that estimate most likely sentences, or fitness applications that estimate heart-rate - require software engineers to design their applications taking into account unpredictable and volatile operational conditions, and noisy data, despite the limited support provided by current unintuitive design and quality assurance methodologies. Finally, the hardware community is designing devices that trade result accuracy for computational efficiency and energy saving, providing only probabilistic guarantees on the correctness of the computed results.
Several research communities are independently investigating methodologies and techniques to model, analyze, and manage uncertainty in and through software systems. These areas include (1) probabilistic model checking, (2) quantitative software analysis, (3) probabilistic programming, and (4) approximate computing. However, despite the substantial overlap of interests, researchers from different communities rarely have the opportunity to meet at conferences typically tailored to single specific areas. Therefore, we organized this seminar as a forum for industrial and academic researchers from these areas to share their recent ideas, identify the main research challenges and future directions, and explore collaborative research opportunities on problems that span across the boundaries of the individual areas.
This report presents a review of each of the main areas covered by the seminar and summarizes the discussions and conclusions of the participants.
The organizers would like to express their gratitude to the participants and the Schloss Dagstuhl team for a productive and exciting seminar. We thank Prof. Martin Rinard for his support and contribution to the organization of the seminar. We thank Sara Achour for her help with preparing this report.
- Sara Achour (MIT - Cambridge, US) [dblp]
- David Bindel (Cornell University, US) [dblp]
- Mateus Araújo Borges (Universität Stuttgart, DE) [dblp]
- James Bornholt (University of Washington - Seattle, US) [dblp]
- Luca Bortolussi (University of Trieste, IT) [dblp]
- Tomáš Brázdil (Masaryk University - Brno, CZ) [dblp]
- Andreas Burg (EPFL - Lausanne, CH) [dblp]
- Luis Ceze (University of Washington - Seattle, US) [dblp]
- Eva Darulova (MPI-SWS - Saarbrücken, DE) [dblp]
- Alessandra Di Pierro (University of Verona, IT) [dblp]
- Luis Maria Ferrer Fioriti (Universität des Saarlandes, DE) [dblp]
- Antonio Filieri (Imperial College London, GB) [dblp]
- Jaco Geldenhuys (University of Stellenbosch, ZA) [dblp]
- Andreas Gerstlauer (University of Texas - Austin, US) [dblp]
- Lars Grunske (HU Berlin, DE) [dblp]
- Jane Hillston (University of Edinburgh, GB) [dblp]
- Ulya R. Karpuzcu (University of Minnesota - Minneapolis, US) [dblp]
- Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
- Marta Kwiatkowska (University of Oxford, GB) [dblp]
- Rupak Majumdar (MPI-SWS - Kaiserslautern, DE) [dblp]
- Dimitrios Milios (University of Edinburgh, GB) [dblp]
- Sasa Misailovic (MIT - Cambridge, US) [dblp]
- Subhasish Mitra (Stanford University, US) [dblp]
- Todd Mytkowicz (Microsoft Corporation - Redmond, US) [dblp]
- Ravi Nair (IBM TJ Watson Research Center - Yorktown Heights, US) [dblp]
- Karthik Pattabiraman (University of British Columbia - Vancouver, CA) [dblp]
- Adrian Sampson (University of Washington - Seattle, US) [dblp]
- Karin Strauss (Microsoft Corporation - Redmond, US) [dblp]
- Willem Visser (Stellenbosch University - Matieland, ZA) [dblp]
- Herbert Wiklicky (Imperial College London, GB) [dblp]
- programming languages / compiler
- software engineering
- verification / logic
- Model Checking
- Program Analysis