Space-Efficient Bounded Model Checking

Details Space-Efficient Bounded Model Checking Space-Efficient Bounded Model Checking

2007-10-25

arxiv.org/abs/0710.4629v1

Dans Design, Automation and Test in Europe - DATE'05, Munich : Allemagne (2005)

Computer Science

Logic in Computer Science

Submitted on behalf of EDAA (http://www.edaa.com/)

Scientific paper

10.1109/DATE.2005.276

Current algorithms for bounded model checking use SAT methods for checking satisfiability of Boolean formulae. These methods suffer from the potential memory explosion problem. Methods based on the validity of Quantified Boolean Formulae (QBF) allow an exponentially more succinct representation of formulae to be checked, because no "unrolling" of the transition relation is required. These methods have not been widely used, because of the lack of an efficient decision procedure for QBF. We evaluate the usage of QBF in bounded model checking (BMC), using general-purpose SAT and QBF solvers. We develop a special-purpose decision procedure for QBF used in BMC, and compare our technique with the methods using general-purpose SAT and QBF solvers on real-life industrial benchmarks.

Affiliated with

Also associated with

No associations

Rating

Space-Efficient Bounded Model Checking does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Space-Efficient Bounded Model Checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Space-Efficient Bounded Model Checking will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-431387