Presenter
Csanád Telbisz
BME, Budapest
Authors
Csanád Telbisz
Abstract
Formal verification of concurrent software faces two major challenges: the state space explosion problem from data complexity, and the combinatorial explosion of thread interleavings. Abstraction and partial order reduction (POR) are well-established techniques for addressing these challenges individually. However, even their orthogonal application - when applying a traditional partial order reduction algorithm on an abstract state space - is not trivially sound. The talk presents a motivating example demonstrating the non-triviality of the combination of these techniques and outlines why this combination is still sound. Furthermore, partial order reduction can be extended to take abstraction into account to achieve further state space reduction. Specifically, the dependency relation used to decide the commutativity of actions for partial order reduction can be relaxed to ignore dependencies when the source of dependency (e.g., a shared variable) is invisible in the abstraction. Experiments reveal that this abstraction-aware extension is as powerful as the applied abstraction: the more details ignored by the abstraction, the better reduction is achieved.
Slides
TBA