BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Michael Weber\, University of Twente\; Microsoft Research Lectures
  - Michael Weber - University of Twente
DTSTART:20100315T140000Z
DTEND:20100315T150000Z
UID:TALK23789@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:*Abstract:* Embedded systems are ubiquitous in everyday applia
 nces\, ranging from washing machines to cars. We present a verification ap
 proach for the (often safety-critical) software used in such systems. Embe
 dded systems software is commonly written for specific micro- controller h
 ardware\, in a mixture of C with non-standard compiler extensions and asse
 mbler. A model checking tool for such software must support features like 
 direct memory accesses\, interrupt handling\, inline assembler instruction
 s\, usage of timers\, communication interfaces\, etc. In our approach\, we
  first compile a C program to its binary representation with an unmodified
  standard compiler\, disassemble the resulting binary and feed it into our
  model checking framework. This has the additional benefit of the model ch
 ecker verifying what is actually executed on the micro-controller and thus
  may even catch errors introduced during compilation\, e.g. in one of the 
 compiler`s optimization passes. We show examples of non- trivial errors th
 at can be found with this approach\, and also reflect on its scalability. 
LOCATION:Small public lecture room\, Microsoft Research Ltd\, 7 J J Thomso
 n Avenue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR