Computer Science – Software Engineering
Scientific paper
2009-07-12
Computer Science
Software Engineering
12 pages
Scientific paper
Propositional bounded model checking has been applied successfully to verify embedded software but is limited by the increasing propositional formula size and the loss of structure during the translation. These limitations can be reduced by encoding word-level information in theories richer than propositional logic and using SMT solvers for the generated verification conditions. Here, we investigate the application of different SMT solvers to the verification of embedded software written in ANSI-C. We have extended the encodings from previous SMT-based bounded model checkers to provide more accurate support for finite variables, 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 applications from telecommunications, control systems and medical devices. The experiments show that our approach can analyze larger problems and substantially reduce the verification time.
Cordeiro Lucas
Fischer Bernd
Marques-Silva Joao
No associations
LandOfFree
SMT-Based Bounded Model Checking for Embedded ANSI-C Software 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 SMT-Based Bounded Model Checking for Embedded ANSI-C Software, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and SMT-Based Bounded Model Checking for Embedded ANSI-C Software will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-100156