Michael Weber, University of Twente; Microsoft Research Lectures

Add to your list(s) Download to your calendar using vCal

• Michael Weber - University of Twente
• Monday 15 March 2010, 14:00-15:00
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Abstract: Embedded systems are ubiquitous in everyday appliances, ranging from washing machines to cars. We present a verification approach for the (often safety-critical) software used in such systems. Embedded systems software is commonly written for specific micro- controller hardware, in a mixture of C with non-standard compiler extensions and assembler. A model checking tool for such software must support features like direct memory accesses, interrupt handling, inline assembler instructions, 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 checker 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 that can be found with this approach, and also reflect on its scalability.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.