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...

• Type: Conference
• Year: 2009
• Where: FMCAD
• Authors: Dirk Beyer, Alessandro Cimatti, Alberto Griggio, M. Erkan Keremoglu, Roberto Sebastiani
• Keywords: Art Represent, FMCAD 2009, Formal Methods, Large-block Encoding, Single-block Encoding