Details

Autor(en) / Beteiligte

• Nguyen, Truc L.
• Fischer, Bernd
• La Torre, Salvatore
• Parlato, Gennaro

Titel

Concurrent Program Verification with Lazy Sequentialization and Interval Analysis

Ist Teil von

• Networked Systems, p.255-271

Ort / Verlag

Cham: Springer International Publishing

Link zum Volltext

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• Lazy sequentialization has proven to be one of the most effective techniques for concurrent program verification. The Lazy-CSeq sequentialization tool performs a “lazy” code-to-code translation from a concurrent program into an equivalent non-deterministic sequential program, i.e., it preserves the valuations of the program variables along its executions. The obtained program is then analyzed using sequential bounded model checking tools. However, the sizes of the individual states still pose problems for further scaling. We therefore use abstract interpretation to minimize the representation of the concurrent program’s (shared global and thread-local) state variables. More specifically, we run the Frama-C abstract interpretation tool over the programs constructed by Lazy-CSeq to compute overapproximating intervals for all (original) state variables and then exploit CBMC’s bitvector support to reduce the number of bits required to represent these in the sequentialized program. We have implemented this approach in the last release of Lazy-CSeq and demonstrate the effectiveness of this approach; in particular, we show that it leads to large performance gains for very hard verification problems.