Abstract | ||
---|---|---|
Lazy abstraction with interpolants, also known as the Impact algorithm, is en vogue as a state-of-the-art software model-checking technique for sequential programs. However, a direct extension of the Impact algorithm to concurrent programs is bound to be inefficient as it has to explore all thread interleavings, which leads to control-state explosion. To this end, we present a new algorithm that combines a new, symbolic form of partial-order reduction with Impact. Our algorithm carries out the dependence analysis on-the-fly while constructing the abstraction and is thus able to deal precisely with dynamic dependencies arising from accesses to tables or pointers - a setting where classical static partial-order reduction techniques struggle. We have implemented the algorithm in a prototype tool that analyses concurrent C program with POSIX threads and evaluated it on a number of benchmark programs. To our knowledge, this is the first application of an Impact-like algorithm to concurrent programs. |
Year | DOI | Venue |
---|---|---|
2013 | 10.1109/FMCAD.2013.6679412 | Formal Methods in Computer-Aided Design |
Keywords | Field | DocType |
interpolation,multi-threading,multiprocessing programs,program diagnostics,program verification,POSIX threads,benchmark programs,concurrent C program analysis,control-state explosion,dependence analysis,impact algorithm,lazy abstraction,multithreaded software verification,power-efficient multicore architectures,sequential programs,software model-checking technique,static partial-order reduction techniques,thread interleavings | Pointer (computer programming),Multithreading,Programming language,Abstraction,Computer science,Interpolation,Parallel computing,Dependence analysis,POSIX Threads,Thread (computing),Real-time computing,Software | Conference |
Citations | PageRank | References |
21 | 0.92 | 15 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Björn Wachter | 1 | 326 | 20.09 |
Daniel Kroening | 2 | 3084 | 187.60 |
Joël Ouaknine | 3 | 1481 | 99.25 |