TY  - CONF
AU  - Brizzolari, Francesco
AU  - Melatti, Igor
AU  - Tronci, Enrico
AU  - Della Penna, Giuseppe
PY  - 2007
DA  - 2007//
TI  - Disk Based Software Verification via Bounded Model Checking
BT  - APSEC '07: Proceedings of the 14th Asia-Pacific Software Engineering Conference
SP  - 358
EP  - 365
PB  - IEEE Computer Society
CY  - Washington, DC, USA
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.
SN  - 0-7695-3057-5
L1  - http://mclab.di.uniroma1.it/publications/papers/brizzolari/2007/76_Brizzolari_etal2007.pdf
UR  - https://doi.org/10.1109/APSEC.2007.43
DO  - 10.1109/APSEC.2007.43
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=76), last updated on Sat, 24 Nov 2012 13:48:38 +0100
ID  - Brizzolari_etal2007
ER  -