MOVES Seminar 28 May 2010, 10:00

 

Stephan Falke (Uni Karlsruhe)

 

 

The Low-Level Bounded Model Checker LLBMC

 

 

Formalizing the semantics of programming languages like C or C++ forbounded model checking can be cumbersome if complete coverage of alllanguage features is to be achieved. On the other hand, low-levellanguages that occur during translation (compilation) have a muchsimpler semantics since they are closer to the machine level. It thusmakes sense to use these low-level languages for bounded model checking.This talk presents the low-level bounded model checker LLBMC anddiscusses a highly precise memory model suitable for bounded modelchecking of low-level languages. The method also takes memory protection(malloc/free) into account.