Sciweavers

Share
FMCAD
2009
Springer

Software model checking via large-block encoding

10 years 1 months ago
Software model checking via large-block encoding
Abstract—Several successful approaches to software verificabased on the construction and analysis of an abstract reachability tree (ART). 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 ting abstract states, in addition to conjunctions as used in SBE, we investigate the use of arbitrary Boolean formulas; ting abstract-successor states, in addition to Cartesian e abstraction as used in SB...
Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where FMCAD
Authors Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani
Comments (0)
books