Skip to main content
Conference ProceedingsOPEN ACCESS

LLBMC: Improved bounded model checking of C programs using LLVM: (Competition contribution)

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2013) 7795 LNCS 623-626
DOI: 10.1007/978-3-642-36742-7_48
19Citations
Citations of this article
11Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

LLBMC is a tool for detecting bugs and runtime errors in C and C++ programs. It is based on bounded model checking using an SMT solver and thus achieves bit-accurate precision. A distinguishing feature of LLBMC in contrast to other bounded model checking tools for C programs is that it operates on a compiler intermediate representation and not directly on the source code. © 2013 Springer-Verlag.

Cite

CITATION STYLE

APA

Falke, S., Merz, F., & Sinz, C. (2013). LLBMC: Improved bounded model checking of C programs using LLVM: (Competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7795 LNCS, pp. 623–626). https://doi.org/10.1007/978-3-642-36742-7_48

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free