University of Limerick
Browse

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

Download (532.5 kB)
journal contribution
posted on 2012-12-05, 12:43 authored by Lucas Cordeiro, Bernd Fischer, Joao Marques-Silva
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.

Funding

Earthquake Damageability of Low-Rise Construction

Directorate for Engineering

Find out more...

Study on Aerodynamic Characteristics Control of Slender Body Using Active Flow Control Technique

Japan Society for the Promotion of Science

Find out more...

History

Publication

IEEE Transactions on Software Engineering;38 (4), pp. 957-974

Publisher

IEEE Computer Society

Note

peer-reviewed

Other Funding information

EPSRC, ERC, ORSAS

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.

Language

English

Usage metrics

    University of Limerick

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC