Abstract
We present LLBMC, a bounded model checker for C programs. LLBMC uses the LLVM compiler framework in order to translate C programs into LLVM's intermediate representation (IR). The resulting code is then converted into a logical representation and simplified using rewrite rules. The simplified formula is finally passed to an SMT solver. In contrast to many other tools, LLBMC uses a flat, bit-precise memory model. It can thus precisely model, e.g., memory-based re-interpret casts. © 2012 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Sinz, C., Merz, F., & Falke, S. (2012). LLBMC: A bounded model checker for LLVM’s intermediate representation (competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7214 LNCS, pp. 542–544). https://doi.org/10.1007/978-3-642-28756-5_44
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
