Concurrent Program Verification with Lazy Sequentialization and Interval Analysis
| Autor: | Gennaro Parlato, Bernd Fischer, Salvatore La Torre, Truc L. Nguyen |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Model checking
State variable Theoretical computer science Exploit Computer science 020207 software engineering 02 engineering and technology Abstract interpretation Translation (geometry) Abstract interpretations Bounded model checking Concurrent program Interval analysis Performance Gain Interval arithmetic 020204 information systems Bounded function 0202 electrical engineering electronic engineering information engineering Representation (mathematics) |
| Zdroj: | Networked Systems ISBN: 9783319596464 NETYS |
| DOI: | 10.1007/978-3-319-59647-1_20 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|