====== Dr.rer.nat. Bastian Schlich ====== \\ {{:lehrstuhl:mitarbeiter:schlich.jpg?150|}}\\ \\ schlich[at]embedded[dot]rwth-aachen[dot]de\\ \\ /* {| |- || {{:lehrstuhl:mitarbeiter:schlich.jpg?150|}} || 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) |} {{:lehrstuhl:mitarbeiter:schlich.jpg?150|}}\\ \\ 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) \\ ===== News ===== I am on vacation until September 13 2009. In urgent matters, you can contact [[:en:lehrstuhl:mitarbeiter:brauer|Jörg Brauer]]. */ ===== Personal ===== 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 [[http://www.embedded.rwth-aachen.de/mc_square|[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". ===== Publications ===== ~~NOCACHE~~ ===== Teaching ===== ==== BSc/MSc/Diploma Theses ==== * Counterexample-Guided Abstraction Refinement for Programmable Logic Controllers (Sebastian Biallas) * [[:en:lehre:abschlussarbeiten:DAVK005]] (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) * [[:en:lehre:abschlussarbeiten:implementierung_eines_simulators_fuer_renesas]] (Mudassir Rasool) * [[:en:lehre:abschlussarbeiten:synthesizing_is_simulators_for_model_checking_es_software]] (Ivica Bogosavljevic) * [[:en:lehre:abschlussarbeiten:model_checking_von_anweisungslisten-prgrammen_fuer_speicherprogrammierbare_steuerung_mit_hilfe_von_mc_square]] (Jörg Wernerus) * [[:en:lehre:abschlussarbeiten:parallelisierung_in_mcsquare]] (Stefan Mau) * [[:en:lehre:abschlussarbeiten:erweiterung_der_symbolischen_zustandsdarstellung_in_mc_square]] ([[:en:lehrstuhl:mitarbeiter:kamin]]) * [[:en:lehre:abschlussarbeiten:model_checking_von_sensornetzwerk-knoten_mit_hilfe_von_mc_square]] (Matthias Moers) * [[:en:lehre:abschlussarbeiten:erweiterung_des_model-checkers_mc_square_um_benutzerdefinierte_umgebungen]] ([[:en:lehrstuhl:mitarbeiter:gueckel]]) * [[:en:lehre:abschlussarbeiten:erweiterung_des_model-checkers_mc_square_fuer_den_infineon_xc167_mikcrocontroller]] (Florian Scheuer) * [[:en:lehre:abschlussarbeiten:einsatz_von_statischen_analysen_im_bereich_des_model-checking_von_software_fuer_eingebettete_systeme]] (Jann Löll) * [[:en:lehre:abschlussarbeiten:symbolisches_model-checking_mit_mc_square]] ([[:en:lehrstuhl:mitarbeiter:schommer]]) * [[:en:lehre:abschlussarbeiten:ein_ansatz_zum_model-checking_von_Software_fuer_eingebettete_systeme]] (Michael Rohrbach) * [[:en:lehre:abschlussarbeiten:untersuchungen_zum_anwendungspotential_der_formalen_verifikation]] ([[:en:lehrstuhl:mitarbeiter:polzer]]) * [[:en:lehre:abschlussarbeiten:model_checking_von_matlab_simulink_modellen]] ([[:en:lehrstuhl:mitarbeiter:palczynski]]) ==== Lectures & Seminars ==== * Winter semester 09/10: [[:en:lehre:wise0910:formale_methoden]] (Lecture) * Summer semester 09: [[http://www-i2.informatik.rwth-aachen.de/i2/teaching/|Applying Formal Verification Methods to Embedded Systems]] (Seminar) * Winter semester 08/09: [[:en:lehre:wise0809:seminar_statische_analyse]] (Seminar) * Summer semester 08: [[:en:lehre:sose08:formale_methoden]] (Lecture) * Summer semester 07: [[:en:lehre:sose07:formale_methoden]] (Lecture) * Winter semester 06/07: [[:en:lehre:wise0607:testen_von_eingebetteten_systemen]] (Seminar) * Summer semester 06: [[:en:lehre:sose06:software_award]] * Winter semester 05/06: [[:en:lehre:wise0506:systematische_software_entwicklung]] (Lecture) * Summer semester 05: [[:en:lehre:sose05:formale_methoden]] (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)