Hana Chockler (King’s College, London): Causality and Responsibility for Formal Verification and Beyond
Abstract: In this talk, I will (briefly) introduce the theory of actual causality as defined by Halpern and Pearl. This theory turns out to be extremely useful in various areas of computer science (and also, perhaps surprisingly, psychology) due to a good match between the results it produces and our intuition. I will outline the evolution of the definitions of actual causality and intuitive reasons for the many parameters in the definition using examples from formal verification. I will also introduce the definitions of responsibility and blame, which quantify the definition of causality.
We will look in more detail at the applications of causality to formal verification, namely, explanation of counter-examples, refinement of coverage metrics, and symbolic trajectory evaluation. It is interesting to note that explanation of counter-examples using the definition of actual causality is implemented in an industrial tool and produces results that are usually consistent with the users’ intuition, hence it is a popular and widely used feature of the tool.
Finally, I will briefly discuss recent applications of causality to legal reasoning and to understanding of political phenomena, and will conclude with outlining promising future directions.
The talk is based on many papers written by many people, and is not limited to my own research. The talk is reasonably self-contained.
Bio: Dr. Hana Chockler is a Lecturer in the Department of Informatics, King’s College London. Before joining King’s College in 2013, Hana worked as a Research Staff Member at IBM Research Laboratory in Haifa, in the formal verification group. Her research interests include formal verification of hardware and software, sanity checks for model checking, automatic generation of specification, explanation of counterexamples, connections between concepts in AI and formal verification, and integration of testing and formal methods. Hana holds a Ph.D. in Computer Science from the Hebrew University of Jerusalem, Israel.
Chao Wang (Virginia Tech): Constraint-based Analysis for Verifying and Debugging Concurrent Software
Abstract: 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.
Bio: Chao Wang is an Assistant Professor of the ECE Department of Virginia Tech. He received the ONR Young Investigator award in 2013 and the NSF CAREER award in 2012. His area of specialization is Software Engineering and Formal Methods, with emphasis on concurrency, formal verification, and program synthesis. He published a book and more than fifty papers in top venues of related field including ICSE, FSE, ASE, ISSTA, CAV, PLDI, and POPL. He received the FMCAD Best Paper award in 2013, the ACM SIGSOFT Distinguished Paper award in 2010, the ACM TODAES Best Paper of the Year award in 2008, and the ACM SIGDA Outstanding PhD Dissertation award in 2004. Dr. Wang received his PhD degree from the University of Colorado at Boulder in 2004. From 2004 to 2011, he was a Research Staff Member at NEC Laboratories of America in Princeton, NJ, where he received a Technology Commercialization award in 2006.
