PT Unknown
AU Brizzolari, F
   Melatti, I
   Tronci, E
   Della Penna, G
TI Disk Based Software Verification via Bounded Model Checking
SE APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference
PY 2007
BP 358
EP 365
DI 10.1109/APSEC.2007.43
AB One of the most successful approach to automatic software verification is SAT based bounded model checking (BMC). One of the main factors limiting the size of programs that can be automatically verified via BMC is the huge number of clauses that the backend SAT solver has to process. In fact, because of this, the SAT solver may easily run out of RAM. We present two disk based algorithms that can considerably decrease the number of clauses that a BMC backend SAT solver has to process in RAM. Our experimental results show that using our disk based algorithms we can automatically verify programs that are out of reach for RAM based BMC.
PI Washington, DC, USA
ER