University of Limerick Institutional Repository

SMT-based bounded model checking for embedded ANSI-C software

DSpace Repository

Show simple item record Cordeiro, Lucas Fischer, Bernd Marques-Silva, Joao 2012-12-05T12:43:17Z 2012-12-05T12:43:17Z 2012
dc.description peer-reviewed en_US
dc.description.abstract Propositional bounded model checking has been applied successfully to verify embedded software but remains limited by increasing propositional formula sizes and the loss of high-level information during the translation preventing potential optimizations to reduce the state space to be explored. These limitations can be overcome by encoding high-level information in theories richer than propositional logic and using SMT solvers for the generated verification conditions. Here, we propose the application of different background theories and SMT solvers to the verification of embedded software written in ANSI-C in order to improve scalability and precision in a completely automatic way. We have modified and extended the encodings from previous SMT-based bounded model checkers to provide more accurate support for variables of finite bit width, bit-vector operations, arrays, structures, unions and pointers. We have integrated the CVC3, Boolector, and Z3 solvers with the CBMC front-end and evaluated them using both standard software model checking benchmarks and typical embedded software applications from telecommunications, control systems, and medical devices. The experiments show that our ESBMC model checker can analyze larger problems than existing tools and substantially reduce the verification time. en_US
dc.language.iso eng en_US
dc.publisher IEEE Computer Society en_US
dc.relation info:eu-repo/grantAgreement/EC/FP7/217069 en_US
dc.relation.ispartofseries IEEE Transactions on Software Engineering;38 (4), pp. 957-974
dc.relation.uri 10.1109/TSE.2011.59
dc.rights “© 2012 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. en_US
dc.subject software engineering en_US
dc.subject formal methods en_US
dc.subject verification en_US
dc.subject model checking en_US
dc.title SMT-based bounded model checking for embedded ANSI-C software en_US
dc.type info:eu-repo/semantics/article en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.contributor.sponsor EPSRC en_US
dc.contributor.sponsor ERC en_US
dc.contributor.sponsor ORSAS en_US
dc.relation.projectid EP/EO12973/1 (NOTOS) en_US
dc.relation.projectid EP/F052669/1 (Cadged Code) en_US
dc.relation.projectid ICT/217069(COCONUT) en_US
dc.relation.projectid IST/033709 (VERTIGO) en_US
dc.rights.accessrights info:eu-repo/semantics/openAccess en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


My Account