AG 1, AG 2, AG 3, AG 4, AG 5, SWS   Info

AG Audience

English

30 Minutes

Saarbrücken

Verification of multithreaded programs is difficult. It requires reasoning about state spaces that grow exponentially in the number of concurrent threads. Successful verification techniques based on modular composition of overapproximations of thread behaviors have been designed for this task. These techniques have been traditionally described in assume-guarantee style, which does not admit reasoning about the abstraction properties of the involved compositional argument. Flanagan and Qadeer thread-modular algorithm is a characteristic representative of such techniques. In this paper, we investigate the formalization of this algorithm in the framework of abstract interpretation. We identify the abstraction that the algorithm implements; its definition involves Cartesian products of sets. Our result provides a basis for the systematic study of similar abstractions for dealing with the state explosion problem. As a first step in this direction, we obtain polynomial-time algorithms based on Cartesian abstraction that enjoy increased precision with respect to the Flanagan-Qadeer method. We limit the design space for future polynomial-time algorithms by providing a characterization of minimal precision increase that leads to loss of polynomial-time complexity.

Alexander Malkis

214

--email hidden

passcode not visible

logged in users only

D.2.4 Software/Program Verification, Formal methods, model checking, {Abstract interpretation, concurrency, thread-modular verification, Cartesian abstraction