Loading...

LLBMC: The Low-Level Bounded Model Checker

3,387 views

Loading...

Loading...

Transcript

The interactive transcript could not be loaded.

Loading...

Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Apr 7, 2011

Google Tech Talk (more info below)
February 22, 2011

Presented by Carsten Sinz, Stephan Falke, & Florian Merz, Karlsruhe Institute of Technology, Germany.

ABSTRACT
Producing reliable and secure software is time consuming and cost intensive, and still many software systems suffer from security vulnerabilities or show unintended, faulty behavior.

Testing is currently the predominant method to ascertain software quality, but over the last years formal methods like abstract interpretation or model checking made huge progress and became applicable to real-world software systems. Their promise is to reach a much higher level of software quality with less effort.

In this talk we present a recent method for systematic bug finding in C programs called Bounded Model Checking (BMC) that works fully automatic and achieves a high level of precision.

We present our implementation, LLBMC, which---in contrast to other
tools---doesn't work on the source code level, but employs a compiler intermediate representation (LLVM IR) as a starting point.

It is thus easily adaptable to support verification of other programming languages such as C++ or ObjC. LLBMC also uses a highly precise (untyped) memory model, which allows to reason about heap and stack data accesses.

Moreover, we show how LLBMC can be integrated into the software development process using a technique called Abstract Testing.

Loading...

When autoplay is enabled, a suggested video will automatically play next.

Up next


to add this to Watch Later

Add to

Loading playlists...