Causality-Based Abstract Interpretation = Super-Optimal DPOR + Abstraction

By Marcelo Sousa

Abstract
Causality-based abstract interpretation is a new technique for computing
path-sensitive interference conditions during abstract interpretation of
concurrent programs. In lieu of fixed point computation, it uses prime event
structures to compactly represent causal dependence and interference between
sequences of transformers. 
The main contribution of the approach is an unfolding algorithm equivalent to a
super-optimal DPOR that uses a new notion of independence to avoid redundant
transformer application, thread-local fixed points to reduce the size of the
unfolding, and a novel cutoff criterion based on subsumption to guarantee
termination of the analysis. 
In this talk, I will describe the main ideas behind causality-based AI and
motivate new directions in the application of DPORs to further mitigate the
state explosion problem.

Bio
Marcelo Sousa is a PhD student at University of Oxford under Daniel Kroening
and Luke Ong. He has been investigating redundancy-aware procedures in static
analysis, compiler optimisations and state-space exploration methods with
applications to the state explosion problem in analysis of concurrent systems
and relational verification. 
Marcelo is the sole recipient of the 2016 Google PhD Fellowship in Programming
Languages and Software Engineering.

More information