Disk Based Software Verification via Bounded Model Checking | Zendy

Fernando Brizzolari | Zendy; Igor Melatti | Zendy; Enrico Tronci | Zendy; Giuseppe Della Penna | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Disk Based Software Verification via Bounded Model Checking

Author(s) -

Fernando Brizzolari,

Igor Melatti,

Enrico Tronci,

Giuseppe Della Penna

Publication year - 2007

Publication title -

proceedings - asia pacific software engineering conference/proceedings

Language(s) - English

Resource type - Conference proceedings

SCImago Journal Rank - 0.208

H-Index - 36

eISSN - 2640-0715

pISSN - 1530-1362

ISBN - 0-7695-3057-5

DOI - 10.1109/apsec.2007.43

Subject(s) - computer science , solver , model checking , bounded function , process (computing) , software , limiting , satisfiability modulo theories , parallel computing , software verification , programming language , algorithm , software system , mathematics , software construction , mechanical engineering , mathematical analysis , engineering

One of the most succesfull 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research