Published: 26th August 2016
DOI: 10.4204/EPTCS.224
ISSN: 2075-2180

EPTCS 224

Proceedings First Workshop on
Causal Reasoning for Embedded and safety-critical Systems Technologies
Eindhoven, The Netherlands, 8th April 2016

Edited by: Gregor Gössler and Oleg Sokolsky

Preface
Morning Keynote: Causality and Responsibility for Formal Verification and Beyond
Hana Chockler
1
Afternoon Keynote: Constraint-based Analysis for Verifying and Debugging Concurrent Software
Chao Wang
9
(De-)Composing Causality in Labeled Transition Systems
Georgiana Caltais, Stefan Leue and Mohammad Reza Mousavi
10
Debugging of Markov Decision Processes (MDPs) Models
Hichem Debbi
25
Towards a Unified Model of Accountability Infrastructures
Severin Kacianka, Florian Kelbert and Alexander Pretschner
40
Invited Presentation: Fault Localization in Web Applications via Model Finding
Sylvain Hallé and Oussama Beroual
55

Preface

Formal approaches for automated causality analysis, fault localization, explanation of events, accountability and blaming have been proposed independently by several communities — in particular, AI, concurrency, model-based diagnosis, formal methods. Work on these topics has significantly gained speed during the last years. The goals of CREST are to bring together and foster exchange between researchers from the different communities, and to present and discuss recent advances and new ideas in the field.

The workshop program consisted of a set of invited and contributed presentations that illustrate different techniques for, and applications of, causality analysis and fault localization.

The program was anchored by two keynote talks. The keynote by Hana Chockler (King’s College) provided a broad perspective on the application of causal reasoning based on Halpern and Pearl’s definitions of actual causality to a variety of application domains ranging from formal verification to legal reasoning. The keynote by Chao Wang (Virginia Tech) concentrated on constraint-based analysis techniques for debugging and verifying concurrent programs.

Workshop papers deal with compositional causality analysis and a wide spectrum of application for causal reasoning, such as debugging of probabilistic models, accountability and responsibility, hazard analysis in practice based on Lewis’ counterfactuals, and fault localization and repair.

The program was completed by an informal discussion on open issues in causality analysis.

We would like to thank keynote speakers and the authors of invited and contributed papers, without whom this workshop would not be possible. We also would like to thank the program committee who provided thorough evaluation of the contributions and helpful feedback for the authors. We are grateful to the ETAPS organization committee for the logistical support of the workshop. Additional support was provided by the Causalysis project funded by Inria.

Gregor Gössler and Oleg Sokolsky

Program Committee

Salem Benferhat CRIL Université d’Artois, France
Hana Chockler Kings College, UK
Eric Fabre INRIA, France
Görschwin Fey University of Bremen & DLR, Germany
Gregor Gössler INRIA, France (co-chair)
Alex Groce Oregon State University, USA
Sylvain Hallé University of Quebec at Chicoutimi, Canada
Joseph Halpern Cornell University, USA
Stefan Leue University of Konstanz, Germany
Dejan Nickovic Austrian Institute of Technology, Austria
Andy Podgurski Case Western Reserve University, USA
Oleg Sokolsky University of Pennsylvania, USA (co-chair)
Jean-Bernard Stefani INRIA, France
Louise Travé-Massuyès  LAAS-CNRS, France
Joost Vennekens K.U. Leuven, Belgium
Chao Wang Virginia Tech, USA
Georg Weissenbacher Vienna University of Technology, Austria

Constraint-based Analysis for Verifying and Debugging Concurrent Software

Chao Wang (Virginia Tech, USA)

The use of multi-core architecture is now pervasive, spanning from embedded systems and smart phones, to commodity PCs, all the way to high-end servers and distributed systems. As such, developers must write concurrent software. However, writing correct and efficient concurrent software is difficult. Although automated analysis to aid in their development would be invaluable, existing methods are either fast but inaccurate, or accurate but slow, due to the inherent difficulty in circumventing the path and interleaving explosion problem. In this talk, I will introduce a series of symbolic predictive analysis methods for analyzing concurrent software. This analysis consists of two steps. First, we derive a predictive model from the execution traces collected at run time as well as the software code. The model captures not only the given executions but also the alterative interleavings of events in these executions. Then, we use symbolic analysis to check if errors exist in these alternative interleavings. This is accomplished by capturing these interleavings and the error conditions using a set of logic formulas and deciding them using a Satisfiability Modulo Theory (SMT) solver. Although our primary focus is to reduce the cost associated with analyzing and verifying concurrent software, the predictive model and related analysis techniques are also useful in addressing issues related to performance and security.