schlich[at]embedded[dot]rwth-aachen[dot]de

/*

|

| Research Assistant schlich[at]embedded[dot]rwth-aachen[dot]de If I do not answer an email within reasonable time, please give me a call because your email might be removed by our spam filter. Phone +49 241 80 21158 Fax +49 241 80 6 21158 Address: Ahornstr. 55, 52074 Aachen, Germany Office: room 2325 (Building H)

Postdoc
Group leader of Formal Verification Group

If I do not answer an email within reasonable time, please give me a call because your email might be removed by our spam filter.

Consultation-hour: On Tuesdays 13:00 - 14:00 (please ask for appointment via email)

Email: schlich[at]embedded[dot]rwth-aachen[dot]de
Phone: +49 241 80 21158
Fax: +49 241 80 6 21158

Address: Ahornstr. 55, 52074 Aachen, Germany
Office: room 2325 (Building H)

I am on vacation until September 13 2009. In urgent matters, you can contact Jörg Brauer. */

I worked at the Embedded Software Laboratory from April 2004 until February 2010, first as a PhD student and then as a postdoc. As a postodc, I was leading the Formal Verifiation group. My main research interest was in formal verification of software for embedded systems. The group applies different formal verification techniques such as static analysis, abstract interpretation, and model checking to embedded software.

The group develops a tool for the analysis of assemby code for microcontrollers and instruction list programs for PLCs. The tool is called [mc]square. In the tool, different formal methods such as model checking, abstract interpretation, and static analysis are applied and adapted to the specifics of embedded systems software. The main focus is the application of theoretical results to real problems. The tool should be user-friendly and easy to handle and should not require changes of the program to be analyzed.

In a second project, a static analyzer for C code is developed, which aims at supporting the development of embedded software accoring to the upcoming ISO 26262. It will be implemented as a plugin for the Ecplise development platform. Later, it will be implemented as a plugin for the Microsoft Visual Studio development platform.

I received my Doctoral degree in June 2008 from the RWTH Aachen University. The title of my Dissertation thesis is „Model Checking of Software for Microcontollers“. I wrote my Diploma thesis at the chair of Software-Technology, University of Dortmund. The topic of the thesis is „Konzeption und Realisierung eines Werkzeugs zur Unterstützung des Test-Driven-Developments“.

<BIBTEX: file=publikationen style=I11 sort=year filter=schlich>

• Counterexample-Guided Abstraction Refinement for Programmable Logic Controllers (Sebastian Biallas)
• Extending EVA to 16 and 32 Bit Systems (Michael Lambertz)
• Static Analysis for the Renesas R8C/23 Microcontroller (Jörg Toborg)
• Static Analysis of Microcontroller Programs using SAT- and Constraint-Solving (Lucas Brutschy)
• Implementation of a Simulator for a Renesas Microcontroller (Mudassir Rasool)
• Synthesizing an Instruction Set Simulator for Model Checking Embedded Systems Software (Ivica Bogosavljevic)
• Model-Checking of Instruction List Programs for Programmable Logic Controllers using [mc]square (Jörg Wernerus)
• Parallel and Distributed Construction of the State Spaces in the Model Checker [mc]square (Stefan Mau)
• Extending the Symbolic Representation of States in [mc]square (Dipl.-Inform. Volker Kamin)
• Model-Checking of Sensor Network Nodes with the Help of [mc]square (Matthias Moers)
• Extending the Model Checker [mc]square by User-Defined Environments (Dr. rer. nat. Dominique Marcel Gückel)
• Extending the Model Checker [mc]square to Handle the Infineon XC167 Microcontroller (Florian Scheuer)
• Application of Static Analysis in the Field of Model Checking Software for Embedded Systems (Jann Löll)
• Symbolic Model Checking in [mc]square (Dipl.-Inform. John F. Schommer)
• An Approach for Model Checking Embedded Systems Software (Michael Rohrbach)
• Studies on the Application Potential of Formal Verification in the Engine Management Systems Software Domain (Dr. rer. nat. Andreas Polzer)
• Requirements for a Model Checker for Matlab/Simulink (Dr. rer. nat. Jacob Palczynski)

• Winter semester 09/10: Formal Methods for Embedded Systems (Lecture)
• Summer semester 09: Applying Formal Verification Methods to Embedded Systems (Seminar)
• Winter semester 08/09: Static Analysis of Embedded Systems Software (Seminar)
• Summer semester 08: Formal Methods for Embedded Systems (Lecture)
• Summer semester 07: Formal Methods for Embedded Software (Lecture)
• Winter semester 06/07: Testing Embedded Systems (Seminar)
• Summer semester 06: SUN Software Award 2006
• Winter semester 05/06: Systematic Software Engineering (Lecture)
• Summer semester 05: Formal Methods for Embedded Systems (Lecture)
• Winter semester 04/05: Systems Programming (Lecture)
• Winter semester 04/05: Application of Model Checking to Embedded Systems (Seminar)
• Summer semester 04: Hybrid and Real-Time Systems (Seminar)