Abstract

This talk will cover different formal verification techniques for microcontroller assembly code. All described techniques are implemented in a tool called [mc]square, which is a model checking and static analysis framework for microcontroller assembly code. The talk comprises three parts. The first part will detail different static analysis for microcontroller assembly code. Some of these analyses are generic such as live variables analysis and reaching definitions analysis while others such as stack analysis and interrupt flag analysis are specifically tailored for microcontrollers. The second part will describe model checking of microcontroller assembly code. It will detail the way state spaces are built and explain the model-checking algorithms applied by [mc]square. One of the major challenges in model checking is the state-explosion problem. A way to tackle the state-explosion problem is the application of abstraction techniques. The third part will detail some abstraction techniques with an emphasis on abstraction techniques that are specifically tailored to microcontroller assembly code. Additionally, it will present some case studies, which show the applicability of formal verification techniques to microcontroller assembly code.

Biography

- Working @ Embedded Software Laboratory @ RWTH Aachen University

• Working on verification of embedded software

• Specifically: microcontroller assembly code and instruction list programs for Programmable Logic Controllers

• Received the Bochers Plaktette for his Dissertation Thesis in 2009

• Since July 2008 Postdoc @ Embedded Software Laboratory

• April 2004 - June 2008 Research Assistant at Embedded Software Laboratory

• September 2007 - February 2008 visiting researcher @ National ICT Australia (Sydney)

• 1998 - 2004 studied computer science @ University Dortmund

Speakers

• Dr. Bastian Schlich, RWTH Aachen

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.

Note: This is one of the thousands of items we imported from the old website. We’re in the process of reviewing each and every one, but if you notice something strange about this particular one, please let us know. — Thanks!