Software Model Checking via Large-Block Encoding
| dc.creator | Beyer, Dirk | |
| dc.creator | Cimatti, Alessandro | |
| dc.creator | Griggio, Alberto | |
| dc.creator | Keremoglu, M. Erkan | |
| dc.creator | Sebastiani, Roberto | |
| dc.date | 2009-04-29 | |
| dc.date.accessioned | 2026-07-07T13:10:05Z | |
| dc.date.available | 2026-07-07T13:10:05Z | |
| dc.description | The construction and analysis of an abstract reachability tree (ART) are the basis for a successful method for software verification. The ART represents unwindings of the control-flow graph of the program. Traditionally, a transition of the ART represents a single block of the program, and therefore, we call this approach single-block encoding (SBE). SBE may result in a huge number of program paths to be explored, which constitutes a fundamental source of inefficiency. We propose a generalization of the approach, in which transitions of the ART represent larger portions of the program; we call this approach large-block encoding (LBE). LBE may reduce the number of paths to be explored up to exponentially. Within this framework, we also investigate symbolic representations: for representing abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; for computing abstract-successor states, in addition to Cartesian predicate abstraction as used in SBE, we investigate the use of Boolean predicate abstraction. The new encoding leverages the efficiency of state-of-the-art SMT solvers, which can symbolically compute abstract large-block successors. Our experiments on benchmark C programs show that the large-block encoding outperforms the single-block encoding. | |
| dc.description | 13 pages (11 without cover), 4 figures, 5 tables | |
| dc.identifier | https://arxiv.org/abs/0904.4709 | |
| dc.identifier | http://arxiv.org/abs/0904.4709 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/228946 | |
| dc.subject | Software Engineering | |
| dc.subject | Programming Languages | |
| dc.subject | D.2.4; F.3.1 | |
| dc.title | Software Model Checking via Large-Block Encoding | |
| dc.type | text |