Dr.rer.nat. Bastian Schlich

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

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 [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

Publikations-Export

[BKK+13] PDF BIB

Biallas, S., Kamin, V., Kowalewski, S., Schlich, B., Sehestedt, S., and Stattelmann, S., "Verifikation von sicherheitsgerichteten SPS-Programmen mit Hilfe von Safety-Automaten", in Proc. Automation 2013, 2013 in VDI Berichte, VDI-Verlag, To appear.

Verifikation von sicherheitsgerichteten SPS-Programmen mit Hilfe von Safety-Automaten

Bibtex entry :

@inproceedings { BKK+13,
	author = { Biallas, Sebastian and Kamin, Volker and Kowalewski, Stefan
		and Schlich, Bastian and Sehestedt, Stephan and Stattelmann,
		Stefan },
	editor = { VDI Wissensforum },
	title = { Verifikation von sicherheitsgerichteten SPS-Programmen mit
		Hilfe von Safety-Automaten },
	booktitle = { Automation 2013 },
	series = { VDI Berichte },
	publisher = { VDI-Verlag },
	publishedas = { Druck },
	language = { ger },
	year = { 2013 },
	timestamp = { 2013.04.16 },
	i11key = { conference },
	note = { To appear },
	for_reporting_period = { 2013 },
}

[BKS12a] PDF BIB

Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse von SPS-Programmen", in Proc. AUTOMATION 2012, Baden-Baden, Germany, Düsseldorf, 2012 in VDI-Berichte, VDI-Verlag, pp. 79-83, Long version (12 pages) on CD-ROM.

Automatische Wertebereichsanalyse von SPS-Programmen

Bibtex entry :

@inproceedings { BKS12a,
	address = { D{\"u}sseldorf },
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Automatische Wertebereichsanalyse von SPS-Programmen },
	booktitle = { AUTOMATION 2012, Baden-Baden, Germany },
	publisher = { VDI-Verlag },
	publishedas = { Druck },
	series = { VDI-Berichte },
	number = { 2171 },
	isbn = { 978-3-18-092171-6 },
	language = { ger },
	pages = { 79--83 },
	year = { 2012 },
	timestamp = { 2012.04.20 },
	i11key = { conference },
	for_reporting_period = { 2012 },
	note = { Long version (12 pages) on CD-ROM },
}

[BKS12b] PDF BIB

Biallas, S., Kowalewski, S., and Schlich, B., "Range and Value-Set Analysis for Programmable Logic Controllers", in Proc. Proceedings of the 11th International Workshop on Discrete Event Systems, Guadalajara, Mexico, 2012, IFAC, pp. 378-383.

Range and Value-Set Analysis for Programmable Logic Controllers

Bibtex entry :

@inproceedings { BKS12b,
	address = { Guadalajara, Mexico },
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Range and Value-Set Analysis for Programmable Logic
		Controllers },
	booktitle = { Proceedings of the 11th International Workshop on Discrete
		Event Systems },
	publisher = { IFAC },
	publishedas = { Druck Online },
	isbn = { 978-3-902823-28-1 },
	language = { eng },
	pages = { 378--383 },
	year = { 2012 },
	timestamp = { 2012.06.26 },
	i11key = { conference },
	url = { http://publications.embedded.rwth-aachen.de/file/3x },
	for_reporting_period = { 2012 },
}

[BKS12c] PDF BIB

Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse -- Formale Verifikation für SPS-Programme", Automatisierungstechnische Praxis (atp EDITION), 54. Jahrgang, 7-8/2012, pp. 68-74, 2012

Automatische Wertebereichsanalyse -- Formale Verifikation f{\"u}r SPS-Programme

Bibtex entry :

@article { BKS12c,
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Automatische Wertebereichsanalyse -- Formale Verifikation
		f{\"u}r SPS-Programme },
	journal = { Automatisierungstechnische Praxis (atp EDITION), 54.
		Jahrgang, 7-8/2012 },
	year = { 2012 },
	pages = { 68--74 },
	publisher = { Oldenbourg Industrieverlag },
	publishedas = { Druck },
	issn = { 2190-4111 },
	i11key = { journal },
	language = { ger },
	timestamp = { 2012.08.02 },
	for_reporting_period = { 2012 },
}

[BBKS10] PDF BIB

Biallas, S., Brauer, J., Kowalewski, S., and Schlich, B., "Automatically Deriving Symbolic Invariants for PLC Programs Written in IL", in Proc. FORMS/FORMAT 2010, 2011, Springer Berlin Heidelberg, pp. 237-245.

Automatically Deriving Symbolic Invariants for {PLC} Programs Written in {IL}

Bibtex entry :

@inproceedings { BBKS10,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
		Stefan and Schlich, Bastian },
	title = { Automatically Deriving Symbolic Invariants for {PLC}
		Programs Written in {IL} },
	booktitle = { FORMS/FORMAT 2010 },
	editor = { Schnieder, Eckehard and Tarnai, Geza },
	publisher = { Springer Berlin Heidelberg },
	publishedas = { Druck },
	language = { eng },
	year = { 2011 },
	timestamp = { 2010.08.19 },
	isbn = { 978-3-642-14261-1 },
	pages = { 237--245 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbks10.pdf },
	i11key = { conference },
	for_reporting_period = { 2010 },
}

[BKS11] PDF BIB

Biallas, S., Kowalewski, S., and Schlich, B., "Leistungsfähige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse", in Proc. AUTOMATION 2011, Baden-Baden, Germany, Düsseldorf, 2011 in VDI-Berichte, VDI-Verlag, pp. 67-72.

Leistungsf{\"a}hige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse

Bibtex entry :

@inproceedings { BKS11,
	address = { D{\"u}sseldorf },
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Leistungsf{\"a}hige Verifikation von industriellen
		SPS-Programmen mittels Model-Checking und statischer Analyse },
	booktitle = { AUTOMATION 2011, Baden-Baden, Germany },
	isbn = { 978-3-18-092143-3 },
	issn = { 0083-5560 },
	number = { 2143 },
	pages = { 67--72 },
	publisher = { VDI-Verlag },
	publishedas = { Druck },
	series = { VDI-Berichte },
	language = { eng },
	year = { 2011 },
	timestamp = { 2011.04.20 },
	i11key = { conference },
	for_reporting_period = { 2011 },
}

[SBK11] PDF BIB

Schlich, B., Brauer, J., and Kowalewski, S., "Application of Static Analyses for State Space Reduction to Microcontroller Binary Code", Sci. Comput. Program., vol. 76, iss. 2, pp. 100-118, 2011

Application of Static Analyses for State Space Reduction to Microcontroller Binary Code

Bibtex entry :

@article { SBK11,
	author = { Schlich, Bastian and Brauer, J{\"o}rg and Kowalewski, Stefan },
	title = { Application of Static Analyses for State Space Reduction to
		Microcontroller Binary Code },
	journal = { Sci. Comput. Program. },
	year = { 2011 },
	volume = { 76 },
	number = { 2 },
	pages = { 100--118 },
	issn = { 0167-6423 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:sbk10.pdf },
	i11key = { journal },
	timestamp = { 2010.12.06 },
	for_reporting_period = { 2011 },
}

[BFK+10] PDF BIB

Biallas, S., Frey, G., Kowalewski, S., Schlich, B., and Soliman, D., "Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene", in Proc. Tagungsband Entwicklung und Betrieb komplexer Automatisierungssysteme (EKA 2010), 2010, ifak Magdeburg, pp. 49-57.

Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene

Bibtex entry :

@inproceedings { BFK+10,
	author = { Biallas, Sebastian and Frey, Georg and Kowalewski, Stefan
		and Schlich, Bastian and Soliman, Doaa },
	title = { Formale Verifikation von Sicherheits-Funktionsbausteinen der
		PLCopen auf Modell- und Code-Ebene },
	booktitle = { Tagungsband Entwicklung und Betrieb komplexer
		Automatisierungssysteme (EKA 2010) },
	publisher = { ifak Magdeburg },
	publishedas = { Druck },
	language = { ger },
	pages = { 49--57 },
	year = { 2010 },
	isbn = { 978-3-940961-41-9 },
	location = { Magdeburg, Germany },
	i11key = { conference },
	for_reporting_period = { 2010 },
}

[BNS10] PDF BIB

Brauer, J., Noll, T., and Schlich, B., "Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software", in Proc. Proceedings of the 13th International Workshop on Software and Compilers for Embedded Systems (SCOPES 2010), 2010, ACM.

Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software

Bibtex entry :

@inproceedings { BNS10,
	author = { Brauer, J{\"o}rg and Noll, Thomas and Schlich, Bastian },
	title = { Interval Analysis of Microcontroller Code using Abstract
		Interpretation of Hardware and Software },
	booktitle = { Proceedings of the 13th International Workshop on Software
		and Compilers for Embedded Systems (SCOPES 2010) },
	year = { 2010 },
	publisher = { ACM },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:BNS10.pdf },
	timestamp = { 2010.04.01 },
	i11key = { conference },
	for_reporting_period = { 2010 },
}

[GSBK10] PDF BIB

Gückel, D., Schlich, B., Brauer, J., and Kowalewski, S., "Synthesizing Simulators for Model Checking Microcontroller Binary Code", in Proc. Proceedings of the 13th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2010), 2010, IEEE, pp. 313-316.

Synthesizing Simulators for Model Checking Microcontroller Binary Code

Bibtex entry :

@inproceedings { GSBK10,
	author = { G{\"u}ckel, Dominique and Schlich, Bastian and Brauer,
		J{\"o}rg and Kowalewski, Stefan },
	title = { Synthesizing Simulators for Model Checking Microcontroller
		Binary Code },
	booktitle = { Proceedings of the 13th IEEE International Symposium on
		Design and Diagnostics of Electronic Circuits and Systems
		(DDECS 2010) },
	year = { 2010 },
	publisher = { IEEE },
	pages = { 313--316 },
	owner = { gueckel },
	i11key = { conference },
	url = { http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5491761 },
	timestamp = { 2010.03.08 },
	for_reporting_period = { 2010 },
}

[RHS+10] PDF BIB

Reinbacher, T., Horauer, M., Schlich, B., Brauer, J., and Scheuer, F., "Model Checking Embedded Software of an Industrial Knitting Machine", International Journal of Information Technology, Communications and Convergenceonvergence, pp. 186-205, 2010

Model Checking Embedded Software of an Industrial Knitting Machine

Bibtex entry :

@article { RHS+10,
	author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian
		and Brauer, J{\"o}rg and Scheuer, Florian },
	title = { Model Checking Embedded Software of an Industrial Knitting
		Machine },
	journal = { International Journal of Information Technology,
		Communications and Convergenceonvergence },
	year = { 2010 },
	pages = { 186--205 },
	publisher = { Inderscience Enterprises Ltd },
	publishedas = { Online Druck },
	issn = { 2042-3217 },
	i11key = { journal },
	language = { eng },
	url = { http://inderscience.metapress.com/content/y664g84625r780l0/fulltext.pdf },
	timestamp = { 2010.08.15 },
	for_reporting_period = { 2010 },
}

[Sch10] PDF BIB

Schlich, B., "Model Checking of Software for Microcontrollers", ACM Transactions in Embedded Computing Systems (TECS), vol. 9, iss. 4, pp. 1-27, 2010

Model Checking of Software for Microcontrollers

Bibtex entry :

@article { Sch10,
	author = { Schlich, Bastian },
	journal = { ACM Transactions in Embedded Computing Systems (TECS) },
	title = { Model Checking of Software for Microcontrollers },
	year = { 2010 },
	volume = { 9 },
	number = { 4 },
	pages = { 1--27 },
	issn = { 1539-9087 },
	doi = { http://doi.acm.org/10.1145/1721695.1721702 },
	publisher = { ACM },
	i11key = { journal },
	for_reporting_period = { 2010 },
}

[BHS09] PDF BIB

Brauer, J., Huuck, R., and Schlich, B., "Interprocedural Pointer Analysis in Goanna", Electronic Notes in Theoretical Computer Science, vol. 254, p. 65, 2009, Proceedings of the 4th International Workshop on Systems Software Verification (SSV 2009)

Interprocedural Pointer Analysis in Goanna

Bibtex entry :

@article { BHS09,
	author = { Brauer, J{\"o}rg and Huuck, Ralf and Schlich, Bastian },
	title = { Interprocedural Pointer Analysis in Goanna },
	journal = { Electronic Notes in Theoretical Computer Science },
	volume = { 254 },
	pages = { 65–83 },
	year = { 2009 },
	note = { Proceedings of the 4th International Workshop on Systems
		Software Verification (SSV 2009) },
	publisher = { Elsevier },
	issn = { 1571-0661 },
	url = { http://portal.acm.org/citation.cfm?id=1630458 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[BSK09b] PDF BIB

Brauer, J., Schlich, B., and Kowalewski, S., "Parallel and Distributed Invariant Checking of Microcontroller Software", Electronic Notes in Theoretical Computer Science, vol. 254, p. 45, 2009, Proceedings of the 4th International Workshop on Systems Software Verification (SSV 2009)

Parallel and Distributed Invariant Checking of Microcontroller Software

Bibtex entry :

@article { BSK09b,
	title = { Parallel and Distributed Invariant Checking of
		Microcontroller Software },
	journal = { Electronic Notes in Theoretical Computer Science },
	volume = { 254 },
	pages = { 45–63 },
	year = { 2009 },
	note = { Proceedings of the 4th International Workshop on Systems
		Software Verification (SSV 2009) },
	publisher = { Elsevier },
	issn = { 1571-0661 },
	author = { Brauer, J{\"o}rg and Schlich, Bastian and Kowalewski, Stefan },
	url = { http://portal.acm.org/citation.cfm?id=1630177.1630457 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[BSRK09] PDF BIB

Brauer, J., Schlich, B., Reinbacher, T., and Kowalewski, S., "Stack Bounds Analysis of Microcontroller Assembly Code", in Proc. Workshop on Embedded Security (WESS 2009), Grenoble, France, 2009, ACM Press.

Stack Bounds Analysis of Microcontroller Assembly Code

Bibtex entry :

@inproceedings { BSRK09,
	author = { Brauer, J{\"o}rg and Schlich, Bastian and Reinbacher, Thomas
		and Kowalewski, Stefan },
	title = { Stack Bounds Analysis of Microcontroller Assembly Code },
	booktitle = { Workshop on Embedded Security (WESS 2009), Grenoble, France },
	year = { 2009 },
	publisher = { ACM Press },
	url = { http://portal.acm.org/citation.cfm?id=1631716.1631721 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[FHST09] PDF BIB

Fehnker, A., Huuck, R., Schlich, B., and Tapp, M., "Automatic Bug Detection in Microcontroller Software by Static Program Analysis", in Proc. SOFSEM 2009: Theory and Practise of Computer Science, Spindleruv Mlýn, Czech Republic, 2009, vol. 5404 in Lecture Notes in Computer Science, Springer, pp. 267-278.

Automatic Bug Detection in Microcontroller Software by Static Program Analysis

Bibtex entry :

@inproceedings { FHST09,
	author = { Fehnker, Ansgar and Huuck, Ralf and Schlich, Bastian and
		Tapp, Michael },
	booktitle = { SOFSEM 2009: Theory and Practise of Computer Science,
		Spindleruv Ml\'{y}n, Czech Republic },
	doi = { 10.1007/978-3-540-95891-8_26 },
	isbn = { 978-3-540-95890-1 },
	pages = { 267--278 },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	title = { Automatic Bug Detection in Microcontroller Software by
		Static Program Analysis },
	volume = { 5404 },
	year = { 2009 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[Mit09] PDF BIB

Mitsching, R., "Testing in the Industrial Development Process for Embedded Systems", in Proc. Doctoral Symposium on Systems Software Verification (DS SSV’09) Real Software, Real Problems, Real Solutions, 2009, RWTH Aachen University, pp. 23-25.

Testing in the Industrial Development Process for Embedded Systems

Bibtex entry :

@inproceedings { Mit09,
	author = { Mitsching, Ralf },
	title = { Testing in the Industrial Development Process for Embedded
		Systems },
	booktitle = { Doctoral Symposium on Systems Software Verification (DS
		SSV’09) Real Software, Real Problems, Real Solutions },
	year = { 2009 },
	pages = { 23--25 },
	publisher = { RWTH Aachen University },
	editor = { Ralf Huuck and Gerwin Klein and Bastian Schlich },
	isbn = { 0935-3232 },
	owner = { mitsching },
	timestamp = { 2009.08.10 },
	url = { http://aib.informatik.rwth-aachen.de/2009/2009-14.pdf },
	i11key = { conference },
	for_reporting_period = { 2010 },
}

[RBHS09] PDF BIB

Reinbacher, T., Brauer, J., Horauer, M., and Schlich, B., "Refining Assembly Code Static Analysis for the Intel MCS-51 Microcontroller", in Proc. Industrial Embedded Systems (SIES'09), Lausanne, Switzerland, 2009, IEEE Computer Society Press, pp. 161-170.

Refining Assembly Code Static Analysis for the Intel MCS-51 Microcontroller

Bibtex entry :

@inproceedings { RBHS09,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Schlich, Bastian },
	booktitle = { Industrial Embedded Systems (SIES'09), Lausanne, Switzerland },
	doi = { 10.1109/SIES.2009.5196212 },
	isbn = { 978-1-4244-4109-9 },
	pages = { 161--170 },
	publisher = { IEEE Computer Society Press },
	title = { Refining Assembly Code Static Analysis for the Intel MCS-51
		Microcontroller },
	year = { 2009 },
	url = { http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5196212 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[RHS+09] PDF BIB

Reinbacher, T., Horauer, M., Schlich, B., Brauer, J., and Scheuer, F., "Model Checking Assembly Code of an Industrial Knitting Machine", in Proc. Embedded and Multimedia Computing (EM-Com 2009), Jeju, Korea, 2009, IEEE Computer Society Press, pp. 1-8.

Model Checking Assembly Code of an Industrial Knitting Machine

Bibtex entry :

@inproceedings { RHS+09,
	author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian
		and Brauer, J{\"o}rg and Scheuer, Florian },
	title = { Model Checking Assembly Code of an Industrial Knitting
		Machine },
	booktitle = { Embedded and Multimedia Computing (EM-Com 2009), Jeju, Korea },
	year = { 2009 },
	publisher = { IEEE Computer Society Press },
	pages = { 1--8 },
	i11key = { conference },
	url = { http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5402986 },
	for_reporting_period = { 2010 },
}

[RHS09] PDF BIB

Reinbacher, T., Horauer, M., and Schlich, B., "Using 3-Valued Memory Representation for State Space Reduction in Embedded Assembly Code Model Checking", in Proc. Design and Diagnostics of Electronic Circuits and Systems (DDECS 2009), Liberec, Czech Republic, 2009, IEEE Computer Society Press, pp. 114-119.

Using 3-Valued Memory Representation for State Space Reduction in Embedded Assembly Code Model Checking

Bibtex entry :

@inproceedings { RHS09,
	author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian },
	booktitle = { Design and Diagnostics of Electronic Circuits and Systems
		(DDECS 2009), Liberec, Czech Republic },
	doi = { 10.1109/DDECS.2009.5012109 },
	isbn = { 978-1-4244-3341-4 },
	pages = { 114--119 },
	publisher = { IEEE Computer Society Press },
	title = { Using 3-Valued Memory Representation for State Space
		Reduction in Embedded Assembly Code Model Checking },
	year = { 2009 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[SBWK09] PDF BIB

Schlich, B., Brauer, J., Wernerus, J., and Kowalewski, S., "Direct Model Checking of PLC Programs in IL", in Proc. Dependable Control of Discrete Systems (DCDS'09), Bari, Italy, 2009, pp. 28-33.

Direct Model Checking of {PLC} Programs in {IL}

Bibtex entry :

@inproceedings { SBWK09,
	author = { Schlich, Bastian and Brauer, J{\"o}rg and Wernerus, J{\"o}rg
		and  Kowalewski, Stefan },
	booktitle = { Dependable Control of Discrete Systems (DCDS'09), Bari,
		Italy },
	isbn = { 978-3-902661-44-9 },
	title = { Direct Model Checking of {PLC} Programs in {IL} },
	year = { 2009 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:SBWK09.pdf },
	i11key = { conference },
	pages = { 28--33 },
	for_reporting_period = { Old },
}

[SK09] PDF BIB

Schlich, B. and Kowalewski, S., "Model Checking C Source Code for Embedded Systems", International Journal on Software Tools for Technology Transfer (STTT), vol. 11, iss. 3, pp. 187-202, 2009

Model Checking {C} Source Code for Embedded Systems

Bibtex entry :

@article { SK09,
	author = { Schlich, Bastian and Kowalewski, Stefan },
	doi = { 10.1007/s10009-009-0106-5 },
	issn = { 1433-2779 },
	journal = { International Journal on Software Tools for Technology
		Transfer (STTT) },
	number = { 3 },
	pages = { 187--202 },
	publisher = { Springer },
	read = { No },
	title = { Model Checking {C} Source Code for Embedded Systems },
	volume = { 11 },
	year = { 2009 },
	i11key = { journal },
	for_reporting_period = { Old },
}

[SKW09] PDF BIB

Schlich, B., Kowalewski, S., and Wernerus, J., "Verifikation von SPS-Programmen in AWL mit Hilfe von direktem Model-Checking", in Proc. AUTOMATION 2009, Baden-Baden, Germany, Düsseldorf, 2009 in VDI-Berichte, VDI Verlag.

{Verifikation von SPS-Programmen in AWL mit Hilfe von direktem Model-Checking}

Bibtex entry :

@inproceedings { SKW09,
	address = { D{\"u}sseldorf },
	author = { Schlich, Bastian and Kowalewski, Stefan and Wernerus,
		J{\"o}rg },
	booktitle = { AUTOMATION 2009, Baden-Baden, Germany },
	isbn = { 978-3-18-092067-2 },
	number = { 2067 },
	publisher = { VDI Verlag },
	series = { VDI-Berichte },
	title = { {Verifikation von SPS-Programmen in AWL mit Hilfe von
		direktem Model-Checking} },
	url = { http://publications.embedded.rwth-aachen.de/file/42 },
	year = { 2009 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[SNBB09] PDF BIB

Schlich, B., Noll, T., Brauer, J., and Brutschy, L., "Reduction of Interrupt Handler Executions for Model Checking Embedded Software", in Proc. Haifa Verification Conference (HVC 2009), Haifa, Israel, 2009, vol. 6405 in Lecture Notes in Computer Science, Springer, pp. 5-20.

Reduction of Interrupt Handler Executions for Model Checking Embedded Software

Bibtex entry :

@inproceedings { SNBB09,
	author = { Schlich, B. and Noll, T. and Brauer, J. and Brutschy, L. },
	title = { Reduction of Interrupt Handler Executions for Model Checking
		Embedded Software },
	booktitle = { Haifa Verification Conference (HVC 2009), Haifa, Israel },
	year = { 2009 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:SNBB09.pdf },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	volume = { 6405 },
	pages = { 5--20 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[BKKS08] PDF BIB

Beckers, J., Klünder, D., Kowalewski, S., and Schlich, B., "Direct Support for Model Checking of Abstract State Machines by Utilizing Simulation", in Proc. Abstract State Machines, B and Z (ABZ 2008), London, UK, 2008, vol. 5238 in Lecture Notes in Computer Science, Springer, pp. 112-124.

Direct Support for Model Checking of Abstract State Machines by Utilizing Simulation

Bibtex entry :

@inproceedings { BKKS08,
	author = { Beckers, J{\"o}rg and Kl{\"u}nder, Daniel and Kowalewski,
		Stefan  and Schlich, Bastian },
	booktitle = { Abstract State Machines, B and Z (ABZ 2008), London, UK },
	doi = { 10.1007/978-3-540-87603-8_10 },
	isbn = { 978-3-540-87602-1 },
	pages = { 112--124 },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	title = { Direct Support for Model Checking of Abstract State Machines
		by Utilizing  Simulation },
	volume = { 5238 },
	year = { 2008 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[HNSW08] PDF BIB

Herberich, G., Noll, T., Schlich, B., and Weise, C., "Proving Correctness of an Efficient Abstraction for Interrupt Handling", Electronic Notes in Theoretical Computer Science, vol. 217, pp. 133-150, 2008, Proceedings of the 3rd International Workshop on Systems Software Verification (SSV 2008)

Proving Correctness of an Efficient Abstraction for Interrupt Handling

Bibtex entry :

@article { HNSW08,
	author = { Herberich, Gerlind and Noll, Thomas and Schlich, Bastian and
		Weise,  Carsten },
	doi = { 10.1016/j.entcs.2008.06.046 },
	issn = { 1571-0661 },
	journal = { Electronic Notes in Theoretical Computer Science },
	note = { Proceedings of the 3rd International Workshop on Systems
		Software  Verification (SSV 2008) },
	pages = { 133--150 },
	publisher = { Elsevier },
	title = { Proving Correctness of an Efficient Abstraction for
		Interrupt Handling },
	volume = { 217 },
	year = { 2008 },
	i11key = { journal },
	for_reporting_period = { Old },
}

[NS08] PDF BIB

Noll, T. and Schlich, B., "Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code", in Proc. Hardware and Software: Verification and Testing (HVC 2007), Haifa, Israel, 2008, vol. 4899 in Lecture Notes in Computer Science, Springer, pp. 185-201.

Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code

Bibtex entry :

@inproceedings { NS08,
	author = { Noll, Thomas and Schlich, Bastian },
	booktitle = { Hardware and Software: Verification and Testing (HVC 2007),
		Haifa,  Israel },
	doi = { 10.1007/978-3-540-77966-7_16 },
	isbn = { 978-3-540-77964-3 },
	issn = { 0302-9743 },
	pages = { 185--201 },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	title = { Delayed Nondeterminism in Model Checking Embedded Systems
		Assembly  Code },
	volume = { 4899 },
	year = { 2008 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[RKHS08a] PDF BIB

Reinbacher, T., Kramer, M., Horauer, M., and Schlich, B., "Challenges in Embedded Model Checking --- A Simulator for the [mc]square Model Checker", in Proc. Industrial Embedded Systems (SIES 2008), Le Grande Motte, France, 2008, IEEE Computer Society Press, pp. 245-248.

Challenges in Embedded Model Checking --- A Simulator for the [mc]square Model Checker

Bibtex entry :

@inproceedings { RKHS08a,
	author = { Reinbacher, Thomas and Kramer, Michael and Horauer, Martin
		and Schlich,  Bastian },
	booktitle = { Industrial Embedded Systems (SIES 2008), Le Grande Motte,
		France },
	doi = { 10.1109/SIES.2008.4577709 },
	isbn = { 978-1-4244-1994-4 },
	pages = { 245--248 },
	publisher = { IEEE Computer Society Press },
	title = { Challenges in Embedded Model Checking --- A Simulator for
		the [mc]square  Model Checker },
	year = { 2008 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[RKHS08b] PDF BIB

Reinbacher, T., Kramer, M., Horauer, M., and Schlich, B., "Motivating Model Checking for Embedded Systems Software", in Proc. Mechatronic and Embedded Systems and Applications (MESA08), Beijing, China, 2008, IEEE Computer Society Press, pp. 546-551.

Motivating Model Checking for Embedded Systems Software

Bibtex entry :

@inproceedings { RKHS08b,
	author = { Reinbacher, Thomas and Kramer, Michael and Horauer, Martin
		and Schlich,  Bastian },
	booktitle = { Mechatronic and Embedded Systems and Applications (MESA08),
		Beijing,  China },
	doi = { 10.1109/MESA.2008.4735653 },
	isbn = { 978-1-4244-2367-5 },
	pages = { 546--551 },
	publisher = { IEEE Computer Society Press },
	title = { Motivating Model Checking for Embedded Systems Software },
	year = { 2008 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[Sch08] PDF BIB

Schlich, B., "Model Checking of Software for Microcontrollers," PhD Thesis , Aachen, Germany, 2008.

Model Checking of Software for Microcontrollers

Bibtex entry :

@phdthesis { Sch08,
	address = { Aachen, Germany },
	author = { Schlich, Bastian },
	issn = { 0935-3232 },
	month = { June },
	school = { RWTH Aachen University },
	title = { Model Checking of Software for Microcontrollers },
	type = { Dissertation },
	url = { http://aib.informatik.rwth-aachen.de/2008/2008-14.pdf },
	year = { 2008 },
	i11key = { thesis },
	for_reporting_period = { Old },
}

[SGK08] PDF BIB

Schlich, B., Gückel, D., and Kowalewski, S., "Modeling the Environment of Microcontrollers to Tackle the State-Explosion Problem in Model Checking", in Proc. Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2008), Budapest, Hungary, Budapest, Hungary, 2008, L'Harmattan, pp. 27-34.

Modeling the Environment of Microcontrollers to Tackle the State-Explosion Problem in Model Checking

Bibtex entry :

@inproceedings { SGK08,
	address = { Budapest, Hungary },
	author = { Schlich, Bastian and G{\"u}ckel, Dominique and Kowalewski,
		Stefan },
	booktitle = { Formal Methods for Automation and Safety in Railway and
		Automotive  Systems (FORMS/FORMAT 2008), Budapest, Hungary },
	editor = { Tarnai, G. and Schnieder, E. },
	isbn = { 978-963-236-138-3 },
	pages = { 27--34 },
	publisher = { L'Harmattan },
	title = { Modeling the Environment of Microcontrollers to Tackle the
		State-Explosion  Problem in Model Checking },
	year = { 2008 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[SLK08] PDF BIB

Schlich, B., Löll, J., and Kowalewski, S., "Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code", in Proc. Formal Methods for Industrial Critical Systems (FMICS 2007), Berlin, Germany, 2008, vol. 4916 in Lecture Notes in Computer Science, Springer, pp. 21-37.

Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code

Bibtex entry :

@inproceedings { SLK08,
	author = { Schlich, Bastian and L{\"o}ll, Jann and Kowalewski, Stefan },
	booktitle = { Formal Methods for Industrial Critical Systems (FMICS 2007),
		Berlin,  Germany },
	doi = { 10.1007/978-3-540-79707-4_4 },
	isbn = { 978-3-540-79706-7 },
	pages = { 21--37 },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	title = { Application of Static Analyses for State Space Reduction to
		Microcontroller  Assembly Code },
	volume = { 4916 },
	year = { 2008 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[SK07f] PDF BIB

Schlich, B. and Kowalewski, S., "An Extendable Architecture for Model Checking Hardware-Specific Automotive Microcontroller Code", in Proc. Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2007), Braunschweig, Germany, Braunschweig, Germany, 2007, GZVB, pp. 202-212.

An Extendable Architecture for Model Checking Hardware-Specific Automotive Microcontroller Code

Bibtex entry :

@inproceedings { SK07f,
	address = { Braunschweig, Germany },
	author = { Schlich, Bastian and Kowalewski, Stefan },
	booktitle = { Formal Methods for Automation and Safety in Railway and
		Automotive  Systems (FORMS/FORMAT 2007), Braunschweig,
		Germany },
	editor = { Schnieder, E. and Tarnai, G. },
	isbn = { 978-3-937655-09-3 },
	pages = { 202--212 },
	publisher = { GZVB },
	title = { An Extendable Architecture for Model Checking
		Hardware-Specific Automotive Microcontroller Code },
	year = { 2007 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[SSK07] PDF BIB

Schlich, B., Salewski, F., and Kowalewski, S., "Applying Model Checking to an Automotive Microcontroller Application", in Proc. Industrial Embedded Systems (SIES'07), Lisbon, Portugal, 2007, IEEE Computer Society Press, pp. 209-216.

Applying Model Checking to an Automotive Microcontroller Application

Bibtex entry :

@inproceedings { SSK07,
	author = { Schlich, , Bastian and Salewski, Falk and Kowalewski, Stefan },
	booktitle = { Industrial Embedded Systems (SIES'07), Lisbon, Portugal },
	doi = { 10.1109/SIES.2007.4297337 },
	isbn = { 1-4244-0840-7 },
	pages = { 209--216 },
	publisher = { IEEE Computer Society Press },
	title = { Applying Model Checking to an Automotive Microcontroller
		Application },
	year = { 2007 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[PSK06] PDF BIB

Palczynski, J., Schlich, B., and Kowalewski, S., "Eine Evaluationssuite zur schnellen Bewertung von Matlab/Simulink-Modelcheckern", in Proc. Informatik 2006: Informatik für Menschen (INFORMATIK 2006), Dresden, Germany, 2006, vol. 1 in Lecture Notes in Informatics, Gesellschaft für Informatik e.V., pp. 751-755.

{Eine Evaluationssuite zur schnellen Bewertung von Matlab/Simulink-Modelcheckern}

Bibtex entry :

@inproceedings { PSK06,
	author = { Palczynski, Jacob and Schlich, Bastian and Kowalewski,
		Stefan },
	booktitle = { Informatik 2006: Informatik f{\"u}r Menschen (INFORMATIK
		2006), Dresden,  Germany },
	isbn = { 978-3-88579-187-4 },
	issn = { 1617-5468 },
	number = { P-93 },
	pages = { 751--755 },
	publisher = { Gesellschaft f{\"u}r Informatik e.V. },
	series = { Lecture Notes in Informatics },
	title = { {Eine Evaluationssuite zur schnellen Bewertung von
		Matlab/Simulink-Modelcheckern} },
	volume = { 1 },
	year = { 2006 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[SK06b] PDF BIB

Schlich, B. and Kowalewski, S., "[mc]square: A model checker for microcontroller code", in Proc. Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006), Paphos, Cyprus, 2006, IEEE Computer Society Press, pp. 466-473.

[mc]square: A model checker for microcontroller code

Bibtex entry :

@inproceedings { SK06b,
	author = { Schlich, Bastian and Kowalewski, Stefan },
	booktitle = { Leveraging Applications of Formal Methods, Verification and
		Validation (ISoLA 2006), Paphos, Cyprus },
	doi = { 10.1109/ISoLA.2006.62 },
	isbn = { 978-0-7695-3071-0 },
	pages = { 466--473 },
	publisher = { IEEE Computer Society Press },
	title = { [mc]square: A model checker for microcontroller code },
	year = { 2006 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[SRWK06] PDF BIB

Schlich, B., Rohrbach, M., Weber, M., and Kowalewski, S., "Model Checking Software for Microcontrollers", RWTH Aachen University, Aachen, Germany, AIB-2006-11, 2006.

Model Checking Software for Microcontrollers

Bibtex entry :

@techreport { SRWK06,
	address = { Aachen, Germany },
	author = { Schlich, Bastian and Rohrbach, Michael and Weber, Michael
		and Kowalewski, Stefan },
	institution = { RWTH Aachen University },
	issn = { 0935-3232 },
	number = { AIB-2006-11 },
	title = { Model Checking Software for Microcontrollers },
	url = { http://aib.informatik.rwth-aachen.de/2006/2006-11.pdf },
	year = { 2006 },
	for_reporting_period = { Old },
}

[SK05] PDF BIB

Schlich, B. and Kowalewski, S., "Model Checking C Source Code for Embedded Systems", in Proc. IEEE/NASA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA 2005), Columbia, Maryland, USA, Maryland, USA, 2005, NASA, pp. 65-77, NASA/CP-2005-212788.

Model Checking {C} Source Code for Embedded Systems

Bibtex entry :

@inproceedings { SK05,
	address = { Maryland, USA },
	author = { Schlich, Bastian and Kowalewski, Stefan },
	booktitle = { IEEE/NASA Workshop on Leveraging Applications of Formal
		Methods,  Verification, and Validation (ISoLA 2005),
		Columbia, Maryland, USA },
	month = { September },
	note = { NASA/CP-2005-212788 },
	pages = { 65--77 },
	publisher = { NASA },
	title = { Model Checking {C} Source Code for Embedded Systems },
	year = { 2005 },
	i11key = { conference },
	for_reporting_period = { Old },
}

[SK04] PDF BIB

Schlich, B. and Kowalewski, S., "C Model Checker: Eine Übersicht", Embedded Software Laboratory, RWTH Aachen University, Aachen, Germany, RWTH-I11-2004-1, 2004.

{C Model Checker: Eine {\"U}bersicht}

Bibtex entry :

@techreport { SK04,
	address = { Aachen, Germany },
	author = { Schlich, Bastian and Kowalewski, Stefan },
	institution = { Embedded Software Laboratory, RWTH Aachen University },
	number = { RWTH-I11-2004-1 },
	title = { {C Model Checker: Eine {\"U}bersicht} },
	year = { 2004 },
	for_reporting_period = { Old },
}

Teaching

BSc/MSc/Diploma Theses

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 (Dipl.-Inform. 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 (Dipl.-Inform. Andreas Polzer)
Requirements for a Model Checker for Matlab/Simulink (Dipl.-Inform. Jacob Palczynski)

Lectures & Seminars

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)

Chair of CS 11

Research

Teaching

Events

Table of Contents

Dr.rer.nat. Bastian Schlich

Personal

Publications

Verifikation von sicherheitsgerichteten SPS-Programmen mit Hilfe von Safety-Automaten

Bibtex entry :

Automatische Wertebereichsanalyse von SPS-Programmen

Bibtex entry :

Range and Value-Set Analysis for Programmable Logic Controllers

Bibtex entry :

Automatische Wertebereichsanalyse -- Formale Verifikation f{\"u}r SPS-Programme

Bibtex entry :

Automatically Deriving Symbolic Invariants for {PLC} Programs Written in {IL}

Bibtex entry :

Leistungsf{\"a}hige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse

Bibtex entry :

Application of Static Analyses for State Space Reduction to Microcontroller Binary Code

Bibtex entry :

Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene

Bibtex entry :

Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software

Bibtex entry :

Synthesizing Simulators for Model Checking Microcontroller Binary Code

Bibtex entry :

Model Checking Embedded Software of an Industrial Knitting Machine

Bibtex entry :

Model Checking of Software for Microcontrollers

Bibtex entry :

Interprocedural Pointer Analysis in Goanna

Bibtex entry :

Parallel and Distributed Invariant Checking of Microcontroller Software

Bibtex entry :

Stack Bounds Analysis of Microcontroller Assembly Code

Bibtex entry :

Automatic Bug Detection in Microcontroller Software by Static Program Analysis

Bibtex entry :

Testing in the Industrial Development Process for Embedded Systems

Bibtex entry :

Refining Assembly Code Static Analysis for the Intel MCS-51 Microcontroller

Bibtex entry :

Model Checking Assembly Code of an Industrial Knitting Machine

Bibtex entry :

Using 3-Valued Memory Representation for State Space Reduction in Embedded Assembly Code Model Checking

Bibtex entry :

Direct Model Checking of {PLC} Programs in {IL}

Bibtex entry :

Model Checking {C} Source Code for Embedded Systems

Bibtex entry :

{Verifikation von SPS-Programmen in AWL mit Hilfe von direktem Model-Checking}

Bibtex entry :

Reduction of Interrupt Handler Executions for Model Checking Embedded Software

Bibtex entry :

Direct Support for Model Checking of Abstract State Machines by Utilizing Simulation

Bibtex entry :

Proving Correctness of an Efficient Abstraction for Interrupt Handling

Bibtex entry :

Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code

Bibtex entry :

Challenges in Embedded Model Checking --- A Simulator for the [mc]square Model Checker

Bibtex entry :

Motivating Model Checking for Embedded Systems Software

Bibtex entry :

Model Checking of Software for Microcontrollers

Bibtex entry :

Modeling the Environment of Microcontrollers to Tackle the State-Explosion Problem in Model Checking

Bibtex entry :

Application of Static Analyses for State Space Reduction to Microcontroller Assembly Code

Bibtex entry :

An Extendable Architecture for Model Checking Hardware-Specific Automotive Microcontroller Code

Bibtex entry :

Applying Model Checking to an Automotive Microcontroller Application

Bibtex entry :

{Eine Evaluationssuite zur schnellen Bewertung von Matlab/Simulink-Modelcheckern}

Bibtex entry :

[mc]square: A model checker for microcontroller code

Bibtex entry :