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
[BSK+15]
Biallas, S., Simon, H., Kowalewski, S., Hauck-Stattelmann, S., and Schlich, B., "Automatische Testfallgenerierung für SPS-Programme mittels Zeilenüberdeckung"Düsseldorf: VDI, 2015, vol. 2258,2, pp. 95-106.

Automatische Testfallgenerierung für SPS-Programme mittels Zeilenüberdeckung

Bibtex entry :

@inbook {  BSK+15,
	author = { Biallas, Sebastian and Simon, Hendrik and Kowalewski, Stefan
		and Hauck-Stattelmann, Stefan and Schlich, Bastian },
	title = { Automatische Testfallgenerierung f{\"u}r SPS-Programme
		mittels Zeilen{\"u}berdeckung },
	booktitle = { Automation 2015 : benefits of change - the future of
		automation ; 16. Branchentreff der Mess- und
		Automatisierungstechnik ; Kongresshaus Baden-Baden, 11. und
		12. Juni 2015 / VDI/VDE-Gesellschaft Mess- und
		Automatisierungstechnik. - Bd. 1 },
	publisher = { VDI },
	pages = { 95-106 },
	volume = { 2258,2 },
	series = { VDI-Berichte },
	year = { 2015 },
	address = { D{\"u}sseldorf },
	organization = { 16. Branchentreff der Mess-und Automatisierungstechnik
		Automation 2015, Baden-Baden (Germany), 2015-06-11 -
		2015-06-12 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-207912 },
	cin = { 122810 / 120000 },
	url = { http://publications.embedded.rwth-aachen.de/file/5r },
}
[HBS+15]
Hauck-Stattelmann, S., Biallas, S., Schlich, B., Kowalewski, S., and Jetley, R., "Analyzing the Restart Behavior of Industrial Control Applications"Springer International Publishing: Cham, 2015, vol. 9109, pp. 585-588.

Analyzing the Restart Behavior of Industrial Control Applications

Bibtex entry :

@inbook {  HBS+15,
	author = { Hauck-Stattelmann, Stefan and Biallas, Sebastian and
		Schlich, Bastian and Kowalewski, Stefan and Jetley, Raoul },
	title = { Analyzing the Restart Behavior of Industrial Control
		Applications },
	booktitle = { FM 2015: formal methods : 20th international symposium,
		Oslo, Norway, June 24 - 26, 2015 ; proceedings / Nikolaj
		Bjørner; Frank de Boer (eds.) },
	publisher = { Cham },
	pages = { 585-588 },
	volume = { 9109 },
	series = { Lecture Notes in Computer Science },
	year = { 2015 },
	address = { Springer International Publishing },
	organization = { 20th International Symposium Formal Methods, Oslo (Norway),
		2015-06-24 - 2015-06-26 },
	doi = { 10.1007/978-3-319-19249-9_38 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-207691 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/541096 },
}
[SFB+15]
Simon, H., Friedrich, N., Biallas, S., Hauck-Stattelmann, S., Schlich, B., and Kowalewski, S., "Automatic test case generation for PLC programs using coverage metrics", in Proc. 2015 IEEE 20th Conference on Emerging Technologies & Factory Automation (ETFA) : 8 - 11 Sept. 2015, City of Luxembourg, Luxembourg / co-sponsored by IEEE ..., Piscataway, NJ, 2015, IEEE, p. 4.

Automatic test case generation for PLC programs using coverage metrics

Bibtex entry :

@inproceedings {  SFB+15,
	author = { Simon, Hendrik and Friedrich, Nico and Biallas, Sebastian
		and Hauck-Stattelmann, Stefan and Schlich, Bastian and
		Kowalewski, Stefan },
	title = { Automatic test case generation for PLC programs using
		coverage metrics },
	booktitle = { 2015 IEEE 20th Conference on Emerging Technologies & Factory
		Automation (ETFA) : 8 - 11 Sept. 2015, City of Luxembourg,
		Luxembourg / co-sponsored by IEEE ... },
	publisher = { IEEE },
	pages = { 4 S. },
	year = { 2015 },
	address = { Piscataway, NJ },
	organization = { 2015 IEEE 20th Conference on Emerging Technologies & Factory
		Automation, Luxembourg (Luxembourg), 2015-09-08 - 2015-09-11 },
	doi = { 10.1109/ETFA.2015.7301602 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-2015-07849 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/565382 },
}
[BKS+14]
Biallas, S., Kowalewski, S., Stattelmann, S., and Schlich, B., "Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code", in Proc. Discrete Event Systems : [Proc. Proceedings of the 12th International Workshop on Discrete Event Systems, Cachan, France, 2014] / Conference Editor: Lesage, Jean-Jacques, Faure, Jean-Marc, Cury, Jose E. R., Lennartson, Bengt, Cachan, France, 2014, IFAC, pp. 400-405.

Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code

Bibtex entry :

@inproceedings {  BKS+14,
	author = { Biallas, Sebastian and Kowalewski, Stefan and Stattelmann,
		Stefan and Schlich, Bastian },
	title = { Efficient Handling of States in Abstract Interpretation of
		Industrial Programmable Logic Controller Code },
	booktitle = { Discrete Event Systems : [Proc. Proceedings of the 12th
		International Workshop on Discrete Event Systems, Cachan,
		France, 2014] / Conference Editor: Lesage, Jean-Jacques,
		Faure, Jean-Marc, Cury, Jose E. R., Lennartson, Bengt },
	publisher = { IFAC },
	pages = { 400-405 },
	year = { 2014 },
	address = { Cachan, France },
	doi = { 10.3182/20140514-3-FR-4046.00065 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-205968 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/443854 },
}
[SKB+14]
Stattelmann, S., Kowalewski, S., Biallas, S., and Schlich, B., "Applying Static Code Analysis on Industrial Controller Code", in Proc. 2014 IEEE [International Conference on] Emerging Technologies and Factory Automation (ETFA 2014) : Barcelona, Spain, 16 - 19 September 2014 / [co-sponsored by Universitat Politècnica de Catalunya - Barcelona Tech (UPC); IEEE Industrial Electronics Society], Piscataway, NJ, 2014, IEEE, p. 4.

Applying Static Code Analysis on Industrial Controller Code

Bibtex entry :

@inproceedings {  SKB+14,
	author = { Stattelmann, Stefan and Kowalewski, Stefan and Biallas,
		Sebastian and Schlich, Bastian },
	title = { Applying Static Code Analysis on Industrial Controller Code },
	booktitle = { 2014 IEEE [International Conference on] Emerging
		Technologies and Factory Automation (ETFA 2014) : Barcelona,
		Spain, 16 - 19 September 2014 / [co-sponsored by Universitat
		Politècnica de Catalunya - Barcelona Tech (UPC); IEEE
		Industrial Electronics Society] },
	publisher = { IEEE },
	pages = { 4 Seiten },
	year = { 2014 },
	address = { Piscataway, NJ },
	organization = { 2014 IEEE [International Conference on] Emerging
		Technologies and Factory Automation, Barcelona (Spain),
		2014-09-16 - 2014-09-19 },
	doi = { 10.1109/ETFA.2014.7005254 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-206434 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/444619 },
}
[BKK+13]
Biallas, S., Kamin, V., Kowalewski, S., Schlich, B., Sehestedt, S., and Stattelmann, S., "Verifikation von sicherheitsgerichteten SPS-Programmen mit Hilfe von Safety-Automaten"Düsseldorf: VDI-Verl., 2013, vol. 2209, pp. 75-79.

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

Bibtex entry :

@inbook {  BKK+13,
	author = { Biallas, Sebastian and Kamin, Volker and Kowalewski, Stefan
		and Schlich, Bastian and Sehestedt, Stephan and Stattelmann,
		Stefan },
	title = { Verifikation von sicherheitsgerichteten SPS-Programmen mit
		Hilfe von Safety-Automaten },
	booktitle = { Automation 2013 : 14. Branchentreff der Mess- und
		Automatisierungstechnik ; Kongresshaus Baden-Baden, 25. und
		26. Juni 2013 / VDI/VDE-Gesellschaft Mess- und
		Automatisierungstechnik },
	publisher = { VDI-Verl. },
	pages = { 75-79 },
	volume = { 2209 },
	series = { VDI-Berichte },
	year = { 2013 },
	address = { D{\"u}sseldorf },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-203699 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/226206 },
}
[BKS12]
Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse von SPS-Programmen", in Proc. Automation 2012 : der 13. Branchentreff der Mess- und Automatisierungstechnik / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik ; Kongress 'Automation 2012' ; 13 (Baden-Baden) ; 2011.06.13-14Branchentreff der Mess- und Automatisierungstechnik, Düsseldorf, 2012 in VDI-Berichte, VDI-Verl., pp. 79-83.

Automatische Wertebereichsanalyse von SPS-Programmen

Bibtex entry :

@inproceedings {  BKS12,
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Automatische Wertebereichsanalyse von SPS-Programmen },
	booktitle = { Automation 2012 : der 13. Branchentreff der Mess- und
		Automatisierungstechnik / VDI/VDE-Gesellschaft Mess- und
		Automatisierungstechnik ; Kongress 'Automation 2012' ; 13
		(Baden-Baden) ; 2011.06.13-14Branchentreff der Mess- und
		Automatisierungstechnik },
	publisher = { VDI-Verl. },
	pages = { 79-83 },
	series = { VDI-Berichte },
	year = { 2012 },
	address = { D{\"u}sseldorf },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-191631 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/120638 },
}
[BKS12a]
Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse -- Formale Verifikation für SPS-Programme", Automatisierungstechnische Praxis : atp, vol. 54, iss. 7/8, pp. 68-74, 2012

Automatische Wertebereichsanalyse -- Formale Verifikation für SPS-Programme

Bibtex entry :

@article {  BKS12a,
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Automatische Wertebereichsanalyse -- Formale Verifikation
		f{\"u}r SPS-Programme },
	journal = { Automatisierungstechnische Praxis : atp },
	publisher = { Oldenbourg Industrieverl. },
	pages = { 68-74 },
	volume = { 54 },
	number = { 7/8 },
	year = { 2012 },
	address = { M{\"u}nchen },
	issn = { 0178-2320 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-015025 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/133988 },
}
[BKS12b]
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,
	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 },
	pages = { 378-383 },
	year = { 2012 },
	address = { Guadalajara, Mexico },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-236327 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752302 },
}
[BSK12]
Brauer, J., Schlich, B., and Kowalewski, S., "Parallel and distributed invariant checking of microcontroller software", Electronic notes in theoretical computer science : ENTCS, vol. 287, pp. 45-63, 2012

Parallel and distributed invariant checking of microcontroller software

Bibtex entry :

@article {  BSK12,
	author = { Brauer, J{\"o}rg and Schlich, Bastian and Kowalewski, Stefan },
	title = { Parallel and distributed invariant checking of
		microcontroller software },
	journal = { Electronic notes in theoretical computer science : ENTCS },
	publisher = { Elsevier Science },
	pages = { 45-63 },
	volume = { 287 },
	year = { 2012 },
	address = { Amsterdam [u.a.] },
	issn = { 1571-0661 },
	doi = { 10.1016/j.entcs.2009.09.059 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-013643 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/132534 },
}
[BBK+11]
Biallas, S., Brauer, J., Kowalewski, S., and Schlich, B., "Automatically Deriving Symbolic Invariants for PLC Programs Written in IL", in Proc. Formal methods for automation and safety in railway and automotive systems : FORMS/FORMAT 2010 ; [8th symposium ; proceedings] / Eckehard Schnieder; Géza Tarnai, eds., Heidelberg [u.a.], 2011, Springer, pp. 237-245.

Automatically Deriving Symbolic Invariants for PLC Programs Written in IL

Bibtex entry :

@inproceedings {  BBK+11,
	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 = { Formal methods for automation and safety in railway and
		automotive systems : FORMS/FORMAT 2010 ; [8th symposium ;
		proceedings] / Eckehard Schnieder; Géza Tarnai, eds. },
	publisher = { Springer },
	pages = { 237-245 },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-14261-1 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-196797 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/126461 },
}
[BKS11]
Biallas, S., Kowalewski, S., and Schlich, B., "Leistungsfähige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse", in Proc. 'Zukunft verantwortungsvoll gestalten' : Automation 2011 ; der 12. Branchentreff der Mess- und Automatisierungstechnik ; Kongress Baden-Baden, 28. und 29. Juni 2011 / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik. [Kongressleiter: Peter Adolphs ...], Düsseldorf, 2011 in VDI-Berichte, VDI-Verl., pp. 67-72.

Leistungsfähige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse

Bibtex entry :

@inproceedings {  BKS11,
	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 = { 'Zukunft verantwortungsvoll gestalten' : Automation 2011 ;
		der 12. Branchentreff der Mess- und Automatisierungstechnik
		; Kongress Baden-Baden, 28. und 29. Juni 2011 /
		VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik.
		[Kongressleiter: Peter Adolphs ...] },
	publisher = { VDI-Verl. },
	pages = { 67-72 },
	series = { VDI-Berichte },
	year = { 2011 },
	address = { D{\"u}sseldorf },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-189475 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/118212 },
}
[RHS+11]
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 convergence, vol. 1, iss. 2, pp. 186-205, 2011

Model checking embedded software of an industrial knitting machine

Bibtex entry :

@article {  RHS+11,
	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 convergence },
	publisher = { Inderscience Publishers },
	pages = { 186-205 },
	volume = { 1 },
	number = { 2 },
	year = { 2011 },
	address = { Geneva },
	issn = { 2042-3217 },
	doi = { 10.1504/IJITCC.2011.039285 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-052838 },
	cin = { 122810 / 120000 },
	url = { http://www.inderscience.com/IJITCC },
}
[SBK11]
Schlich, B., Brauer, J., and Kowalewski, S., "Application of Static Analyses for State-Space Reduction to the Microcontroller Binary Code", Science of computer programming, vol. 76, iss. 2, pp. 100-118, 2011

Application of Static Analyses for State-Space Reduction to the 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
		the Microcontroller Binary Code },
	journal = { Science of computer programming },
	publisher = { Elsevier },
	pages = { 100-118 },
	volume = { 76 },
	number = { 2 },
	year = { 2011 },
	address = { Amsterdam [u.a.] },
	issn = { 0167-6423 },
	doi = { 10.1016/j.scico.2010.03.006 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-062661 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/186222 },
}
[SNB+11]
Schlich, B., Noll, T., Brauer, J., and Brutschy, L., "Reduction of Interrupt Handler Executions for Model Checking Embedded Software", in Proc. Hardware and software: verification and testing : 5th International Haifa Verification Conference, HCV 2009, Haifa, Israel, October 19-22, 2009 : revised selected papers / Kedar Namjoshi ... (eds.), Heidelberg [u.a.], 2011 in Lecture Notes in Computer Science, Springer.

Reduction of Interrupt Handler Executions for Model Checking Embedded Software

Bibtex entry :

@inproceedings {  SNB+11,
	author = { Schlich, Bastian and Noll, Thomas and Brauer, J{\"o}rg and
		Brutschy, Lucas },
	title = { Reduction of Interrupt Handler Executions for Model Checking
		Embedded Software },
	booktitle = { Hardware and software: verification and testing : 5th
		International Haifa Verification Conference, HCV 2009,
		Haifa, Israel, October 19-22, 2009 : revised selected papers
		/ Kedar Namjoshi ... (eds.) },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-19237-1_5 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-187757 },
	cin = { 122810 / 121310 / 120000 },
	url = { http://publications.rwth-aachen.de/record/116214 },
}
[BFK+10]
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. Entwurf komplexer Automatisierungssysteme : EKA 2010 ; Beschreibungsmittel, Methoden, Werkzeuge und Anwendungen ; 11. Fachtagung mit Tutorium, 25. bis 27. Mai 2010 in Magdeburg, Denkfabrik im Wissenschaftshafen / ifak, Institut für Automation und Kommunikation e.V., Magdeburg; Otto-von-Guericke-Universität Magdeburg, Institut für Automatisierungstechnik. [Hrsg.: Ulrich Jumar, Eckehard Schnieder, Christian Diedrich], Magdeburg, 2010, ifak, 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 = { Entwurf komplexer Automatisierungssysteme : EKA 2010 ;
		Beschreibungsmittel, Methoden, Werkzeuge und Anwendungen ;
		11. Fachtagung mit Tutorium, 25. bis 27. Mai 2010 in
		Magdeburg, Denkfabrik im Wissenschaftshafen / ifak, Institut
		f{\"u}r Automation und Kommunikation e.V., Magdeburg;
		Otto-von-Guericke-Universit{\"a}t Magdeburg, Institut
		f{\"u}r Automatisierungstechnik. [Hrsg.: Ulrich Jumar,
		Eckehard Schnieder, Christian Diedrich] },
	publisher = { ifak },
	pages = { 49-57 },
	year = { 2010 },
	address = { Magdeburg },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190099 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/118924 },
}
[BNS10]
Brauer, J., Noll, T., and Schlich, B., "Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software", in Proc. SCOPES '10 Proceedings of the 13th International Workshop on Software & Compilers for Embedded Systems : St. Goar, Germany - June 29-30, 2010, New York, NY, 2010 in ACM Digital Library, 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 = { SCOPES '10 Proceedings of the 13th International Workshop on
		Software & Compilers for Embedded Systems : St. Goar,
		Germany - June 29-30, 2010 },
	publisher = { ACM },
	series = { ACM Digital Library },
	year = { 2010 },
	address = { New York, NY },
	doi = { 10.1145/1811212.1811216 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-191119 },
	cin = { 122810 / 121310 / 120000 },
	url = { http://publications.rwth-aachen.de/record/120063 },
}
[GSB+10]
Gückel, D., Schlich, B., Brauer, J., and Kowalewski, S., "Synthesizing Simulators for Model Checking Microcontroller Binary", in Proc. Proceedings of the 13th IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems : April 14–16, 2010, Vienna, Austria / Sponsored by IEEE Computer Society, Test Technology Techn. Council, In coop. with Dept. of Computer Engineering, Fac. of Informatics, Vienna Univ. of Techn., Piscataway, NJ, 2010, IEEE, pp. 313-316.

Synthesizing Simulators for Model Checking Microcontroller Binary

Bibtex entry :

@inproceedings {  GSB+10,
	author = { G{\"u}ckel, Dominique and Schlich, Bastian and Brauer,
		J{\"o}rg and Kowalewski, Stefan },
	title = { Synthesizing Simulators for Model Checking Microcontroller
		Binary },
	booktitle = { Proceedings of the 13th IEEE Symposium on Design and
		Diagnostics of Electronic Circuits and Systems : April
		14–16, 2010, Vienna, Austria / Sponsored by IEEE Computer
		Society, Test Technology Techn. Council, In coop. with Dept.
		of Computer Engineering, Fac. of Informatics, Vienna Univ.
		of Techn. },
	publisher = { IEEE },
	pages = { 313-316 },
	year = { 2010 },
	address = { Piscataway, NJ },
	doi = { 10.1109/DDECS.2010.5491761 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190385 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/119227 },
}
[RHS+10]
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 convergence, vol. 1, iss. 2, 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 convergence },
	publisher = { Inderscience Publishers },
	pages = { 186-205 },
	volume = { 1 },
	number = { 2 },
	year = { 2010 },
	address = { Genève },
	issn = { 2042-3217 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-064544 },
	cin = { 122810 / 120000 },
	url = { http://inderscience.metapress.com/content/y664g84625r780l0/fulltext.pdf },
}
[Sch10]
Schlich, B., "Model Checking of Software for Microcontrollers", ACM transactions on embedded computing systems : TECS, vol. 9, iss. 4, p. 27, 2010

Model Checking of Software for Microcontrollers

Bibtex entry :

@article {  Sch10,
	author = { Schlich, Bastian },
	title = { Model Checking of Software for Microcontrollers },
	journal = { ACM transactions on embedded computing systems : TECS },
	publisher = { ACM Press },
	pages = { 27 S. },
	volume = { 9 },
	number = { 4 },
	year = { 2010 },
	address = { New York, NY },
	issn = { 1539-9087 },
	doi = { 10.1145/1721695.1721702 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-047530 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/169982 },
}
[BHS09]
Brauer, J., Huuck, R., and Schlich, B., "Interprocedural pointer analysis in Goanna", Electronic notes in theoretical computer science : ENTCS, vol. 254, pp. 65-83, 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 : ENTCS },
	publisher = { Elsevier Science },
	pages = { 65-83 },
	volume = { 254 },
	year = { 2009 },
	address = { Amsterdam [u.a.] },
	issn = { 1571-0661 },
	doi = { 10.1016/j.entcs.2009.09.060 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-013641 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/132532 },
}
[BSR+09]
Brauer, J., Schlich, B., Reinbacher, T., and Kowalewski, S., "Stack bounds analysis of microcontroller assembly code", in Proc. Embedded Systems Week 2009 : CODES+ISSS’09, CASES’09, EMSOFT’09 ; Proceedings of the 2009 international conference on Compilers, architecture, and synthesis for embedded systems ; 2009, Grenoble, France, October 11 - 16, 2009, New York, NY, 2009, ACM Press.

Stack bounds analysis of microcontroller assembly code

Bibtex entry :

@inproceedings {  BSR+09,
	author = { Brauer, J{\"o}rg and Schlich, Bastian and Reinbacher, Thomas
		and Kowalewski, Stefan },
	title = { Stack bounds analysis of microcontroller assembly code },
	booktitle = { Embedded Systems Week 2009 : CODES+ISSS’09, CASES’09,
		EMSOFT’09 ; Proceedings of the 2009 international
		conference on Compilers, architecture, and synthesis for
		embedded systems ; 2009, Grenoble, France, October 11 - 16,
		2009 },
	publisher = { ACM Press },
	year = { 2009 },
	address = { New York, NY },
	doi = { 10.1145/1631716.1631721 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-173253 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/100433 },
}
[FHS+09]
Fehnker, A., Huuck, R., Schlich, B., and Tapp, M., "Automatic bug detection in microcontroller software by static program analysis"Berlin [u.a.]: Springer, 2009, vol. 5404, pp. 267-278.

Automatic bug detection in microcontroller software by static program analysis

Bibtex entry :

@inbook {  FHS+09,
	author = { Fehnker, Ansgar and Huuck, Ralf and Schlich, Bastian and
		Tapp, Michael },
	title = { Automatic bug detection in microcontroller software by
		static program analysis },
	booktitle = { SOFSEM 2009: theory and practice of computer science : 35th
		Conference on Current Trends in Theory and Practice of
		Computer Science, Špindler°uv Mlyń, Czech Republic,
		January 24 - 30, 2009 ; proceedings / Mogens Nielsen ...
		(eds.) },
	publisher = { Springer },
	pages = { 267-278 },
	volume = { 5404 },
	series = { Lecture notes in computer science },
	year = { 2009 },
	address = { Berlin [u.a.] },
	doi = { 10.1007/978-3-540-95891-8_26 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-095395 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/83459 },
}
[KHS09]
Klein, G., Huuck, R., and Schlich, B., "Operating System Verification", Journal of automated reasoning, vol. 42, iss. 2/4, pp. 123-124, 2009

Operating System Verification

Bibtex entry :

@article {  KHS09,
	author = { Klein, Gerwin and Huuck, Ralf and Schlich, Bastian },
	title = { Operating System Verification },
	journal = { Journal of automated reasoning },
	publisher = { Springer },
	pages = { 123-124 },
	volume = { 42 },
	number = { 2/4 },
	year = { 2009 },
	address = { Dordrecht [u.a.] },
	issn = { 0168-7433 },
	doi = { 10.1007/s10817-009-9126-9 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-065212 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/188901 },
}
[RBH+09]
Reinbacher, T., Brauer, J., Horauer, M., and Schlich, B., "Refining assembly code static analysis for the Intel MCS-51 microcontroller", in Proc. 2009 IEEE International Symposium on Industrial Embedded Systems (SIES 2009) : Lausanne, Switzerland, 08 - 10 July 2009 / [sponsored by: IEEE Industrial Electronics Society (IES)]), Piscataway, NJ, 2009, IEEE, pp. 161-170.

Refining assembly code static analysis for the Intel MCS-51 microcontroller

Bibtex entry :

@inproceedings {  RBH+09,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Schlich, Bastian },
	title = { Refining assembly code static analysis for the Intel MCS-51
		microcontroller },
	booktitle = { 2009 IEEE International Symposium on Industrial Embedded
		Systems (SIES 2009) : Lausanne, Switzerland, 08 - 10 July
		2009 / [sponsored by: IEEE Industrial Electronics Society
		(IES)]) },
	publisher = { IEEE },
	pages = { 161-170 },
	year = { 2009 },
	address = { Piscataway, NJ },
	doi = { 10.1109/SIES.2009.5196212 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-172391 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/99425 },
}
[RHS+09]
Reinbacher, T., Horauer, M., Schlich, B., Brauer, J., and Scheuer, F., "Model checking assembly code of an industrial knitting machine", in Proc. Proceedings of the 2009 Fourth International Conference on Embedded and Multimedia Computing : EM-Com 2009 : [December 10-12, 2009, Jeju Island, Korea], Piscataway, NJ, 2009, IEEE, p. 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 = { Proceedings of the 2009 Fourth International Conference on
		Embedded and Multimedia Computing : EM-Com 2009 : [December
		10-12, 2009, Jeju Island, Korea] },
	publisher = { IEEE },
	pages = { 8 S. },
	year = { 2009 },
	address = { Piscataway, NJ },
	doi = { 10.1109/EM-COM.2009.5402986 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-199048 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/129021 },
}
[RHS09]
Reinbacher, T., Horauer, M., and Schlich, B., "Using 3-valued memory representation for state space reduction in embedded assembly code model checking", in Proc. Proceedings of the 2009 IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems : April 15-17, 2009, Liberec, Czech Republic / M. Renovell; IEEE Computer Society ..., Piscataway, N.J.], 2009, IEEE, 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 },
	title = { Using 3-valued memory representation for state space
		reduction in embedded assembly code model checking },
	booktitle = { Proceedings of the 2009 IEEE Symposium on Design and
		Diagnostics of Electronic Circuits and Systems : April
		15-17, 2009, Liberec, Czech Republic / M. Renovell; IEEE
		Computer Society ... },
	publisher = { IEEE },
	pages = { 114-119 },
	year = { 2009 },
	address = { Piscataway, N.J.] },
	doi = { 10.1109/DDECS.2009.5012109 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-172518 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/99559 },
}
[SBW+09]
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 {  SBW+09,
	author = { Schlich, Bastian and Brauer, J{\"o}rg and Wernerus, J{\"o}rg
		and Kowalewski, Stefan },
	title = { Direct Model Checking of {PLC} Programs in {IL} },
	booktitle = { Dependable Control of Discrete Systems (DCDS'09), Bari,
		Italy },
	pages = { 28-33 },
	year = { 2009 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-236337 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752318 },
}
[SK09]
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 },
	title = { Model checking C source code for embedded systems },
	journal = { International journal on software tools for technology
		transfer : STTT },
	publisher = { Springer },
	pages = { 187-202 },
	volume = { 11 },
	number = { 3 },
	year = { 2009 },
	address = { Berlin [u.a.] },
	issn = { 1433-2779 },
	doi = { 10.1007/s10009-009-0106-5 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-013187 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/132064 },
}
[SKW09]
Schlich, B., Kowalewski, S., and Wernerus, J., "Verifikation von SPS-Programmen in AWL mit Hilfe von direktem Model-Checking", in Proc. Automation 2009 : der Automatisierungskongress in Deutschland ; Kongress Baden-Baden, 16. und 17. Juni 2009 ; [10. Branchentreff der Mess- und Automatisierungstechnik] / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik. - 2067, Düsseldorf, 2009 in VDI-Berichte, VDI-Verl., pp. 13-16.

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

Bibtex entry :

@inproceedings {  SKW09,
	author = { Schlich, Bastian and Kowalewski, Stefan and Wernerus,
		J{\"o}rg },
	title = { Verifikation von SPS-Programmen in AWL mit Hilfe von
		direktem Model-Checking },
	booktitle = { Automation 2009 : der Automatisierungskongress in
		Deutschland ; Kongress Baden-Baden, 16. und 17. Juni 2009 ;
		[10. Branchentreff der Mess- und Automatisierungstechnik] /
		VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik. -
		2067 },
	publisher = { VDI-Verl. },
	pages = { 13-16 },
	series = { VDI-Berichte },
	year = { 2009 },
	address = { D{\"u}sseldorf },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-172091 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/99088 },
}
[BKK+08]
Beckers, J., Klünder, D., Kowalewski, S., and Schlich, B., "Direct support for model checking abstract state machines by utilizing simulation"Berlin [u.a.]: Springer, 2008, vol. 5238, pp. 112-124.

Direct support for model checking abstract state machines by utilizing simulation

Bibtex entry :

@inbook {  BKK+08,
	author = { Beckers, J{\"o}rg and Kl{\"u}nder, Daniel and Kowalewski,
		Stefan and Schlich, Bastian },
	title = { Direct support for model checking abstract state machines by
		utilizing simulation },
	booktitle = { Abstract state machines, B and Z : first international
		conference, ABZ 2008, London, UK, September 16-18, 2008 ;
		proceedings / Egon B{\"o}rger ... (eds.) },
	publisher = { Springer },
	pages = { 112-124 },
	volume = { 5238 },
	series = { Lecture Notes in Computer Science },
	year = { 2008 },
	address = { Berlin [u.a.] },
	doi = { 10.1007/978-3-540-87603-8_10 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-095396 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/83460 },
}
[HSW+08]
Herberich, G., Schlich, B., Weise, C., and Noll, T., "Proving correctness of an efficient abstraction for interrupt handling", Electronic notes in theoretical computer science : ENTCS, vol. 217, pp. 133-150, 2008

Proving correctness of an efficient abstraction for interrupt handling

Bibtex entry :

@article {  HSW+08,
	author = { Herberich, Gerlind and Schlich, Bastian and Weise, Carsten
		and Noll, Thomas },
	title = { Proving correctness of an efficient abstraction for
		interrupt handling },
	journal = { Electronic notes in theoretical computer science : ENTCS },
	publisher = { Elsevier Science },
	pages = { 133-150 },
	volume = { 217 },
	year = { 2008 },
	address = { Amsterdam [u.a.] },
	issn = { 1571-0661 },
	doi = { 10.1016/j.entcs.2008.06.046 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-012122 },
	cin = { 122810 / 121310 / 120000 },
	url = { http://publications.rwth-aachen.de/record/130980 },
}
[NS08]
Noll, T. and Schlich, B., "Delayed nondeterminism in model checking embedded systems assembly code"Berlin [u.a.]: Springer, 2008, vol. 4899, pp. 185-201.

Delayed nondeterminism in model checking embedded systems assembly code

Bibtex entry :

@inbook {  NS08,
	author = { Noll, Thomas and Schlich, Bastian },
	title = { Delayed nondeterminism in model checking embedded systems
		assembly code },
	booktitle = { Hardware and software: verification and testing : third
		International Haifa Verification Conference, HVC 2007,
		Haifa, Israel, October 23 - 25, 2007 ; proceedings / Karen
		Yorav (ed.) },
	publisher = { Springer },
	pages = { 185-201 },
	volume = { 4899 },
	series = { Lecture notes in computer science },
	year = { 2008 },
	address = { Berlin [u.a.] },
	doi = { 10.1007/978-3-540-77966-7_16 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-095397 },
	cin = { 120000 / 122810 / 121310 },
	url = { http://publications.rwth-aachen.de/record/83461 },
}
[RKH+08]
Reinbacher, T., Kramer, M., Horauer, M., and Schlich, B., "Motivating model checking for embedded systems software", in Proc. 2008 IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications : MESA ; Beijing, China, 12 - 15 October 2008, Piscataway, NJ, 2008, IEEE, pp. 546-551.

Motivating model checking for embedded systems software

Bibtex entry :

@inproceedings {  RKH+08,
	author = { Reinbacher, Thomas and Kramer, Michael and Horauer, Martin
		and Schlich, Bastian },
	title = { Motivating model checking for embedded systems software },
	booktitle = { 2008 IEEE/ASME International Conference on Mechatronic and
		Embedded Systems and Applications : MESA ; Beijing, China,
		12 - 15 October 2008 },
	publisher = { IEEE },
	pages = { 546-551 },
	year = { 2008 },
	address = { Piscataway, NJ },
	doi = { 10.1109/MESA.2008.4735653 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-172092 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/99089 },
}
[RKH+08a]
Reinbacher, T., Kramer, M., Horauer, M., and Schlich, B., "Challenges in embedded model checking : a simulator for the [mc]square model checker", in Proc. 2008 International Symposium on Industrial Embedded Systems : [SIES'2008] ; La Grande Motte, France, 11 - 13 June 2008 / IEEE, Piscataway, NJ, 2008, IEEE, pp. 245-248.

Challenges in embedded model checking : a simulator for the [mc]square model checker

Bibtex entry :

@inproceedings {  RKH+08a,
	author = { Reinbacher, Thomas and Kramer, Michael and Horauer, Martin
		and Schlich, Bastian },
	title = { Challenges in embedded model checking : a simulator for the
		[mc]square  model checker },
	booktitle = { 2008 International Symposium on Industrial Embedded Systems
		: [SIES'2008] ; La Grande Motte, France, 11 - 13 June 2008 /
		IEEE },
	publisher = { IEEE },
	pages = { 245-248 },
	year = { 2008 },
	address = { Piscataway, NJ },
	doi = { 10.1109/SIES.2008.4577709 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-172528 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/99569 },
}
[Sch08]
Schlich, B., "Model checking of software for microcontrollers", PhD Thesis, Aachen, 2008.

Model checking of software for microcontrollers

Bibtex entry :

@phdthesis {  Sch08,
	author = { Schlich, Bastian },
	othercontributors = { Kowalewski, Stefan },
	title = { Model checking of software for microcontrollers },
	publisher = { RWTH Aachen, Department of Computer Science },
	pages = { IV, 159 S. : graph. Darst. },
	series = { Aachener Informatik-Berichte },
	year = { 2008 },
	address = { Aachen },
	typ = { PUB:(DE-HGF)11 },
	reportid = { RWTH-CONV-125168 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/63747/files/Schlich_Bastian.pdf },
}
[SGK08]
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 ; proceedings of Symposium FORMS/FORMAT 2008, Budapest, Hungary, October 9 - 10, 2008 / Géza Tarnai ... (ed.), Budapest, 2008, L Harmattan.

Modeling the environment of microcontrollers to tackle the state-explosion problem in model checking

Bibtex entry :

@inproceedings {  SGK08,
	author = { Schlich, Bastian and G{\"u}ckel, Dominique and Kowalewski,
		Stefan },
	title = { Modeling the environment of microcontrollers to tackle the
		state-explosion problem in model checking },
	booktitle = { Formal methods for automation and safety in railway and
		automotive systems ; proceedings of Symposium FORMS/FORMAT
		2008, Budapest, Hungary, October 9 - 10, 2008 / Géza Tarnai
		... (ed.) },
	publisher = { L Harmattan },
	year = { 2008 },
	address = { Budapest },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-171805 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/98749 },
}
[SLK08]
Schlich, B., Löll, J., and Kowalewski, S., "Application of static analyses for state space reduction to microcontroller assembly code"Berlin [u.a.]: Springer, 2008, vol. 4916, pp. 21-37.

Application of static analyses for state space reduction to microcontroller assembly code

Bibtex entry :

@inbook {  SLK08,
	author = { Schlich, Bastian and L{\"o}ll, Jann and Kowalewski, Stefan },
	title = { Application of static analyses for state space reduction to
		microcontroller assembly code },
	booktitle = { Formal methods for industrial critical systems : 12th
		international workshop, FMICS 2007, Berlin, Germany, July 1
		- 2, 2007 ; revised selected papers / Stefan Leue; Pedro
		Merino (eds.) },
	publisher = { Springer },
	pages = { 21-37 },
	volume = { 4916 },
	series = { Lecture notes in computer science },
	year = { 2008 },
	address = { Berlin [u.a.] },
	doi = { 10.1007/978-3-540-79707-4_4 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-095398 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/83462 },
}
[SK07d]
Schlich, B. and Kowalewski, S., "An extendable architecture for model checking hardware-specific automotive microcontroller code", in Proc. FORMS/FORMAT 2007 - 6th symposium : formal methods for automation and safety in railway and automotive systems ; proceedings of Symposium FORMS/FORMAT 2007, Braunschweig, Germany, 25th and 26th January, 2007 / Eckehard Schnieder; Géza Tarnai (Eds.), Braunschweig, 2007, GZVB, pp. 202-212.

An extendable architecture for model checking hardware-specific automotive microcontroller code

Bibtex entry :

@inproceedings {  SK07d,
	author = { Schlich, Bastian and Kowalewski, Stefan },
	title = { An extendable architecture for model checking
		hardware-specific automotive microcontroller code },
	booktitle = { FORMS/FORMAT 2007 - 6th symposium : formal methods for
		automation and safety in railway and automotive systems ;
		proceedings of Symposium FORMS/FORMAT 2007, Braunschweig,
		Germany, 25th and 26th January, 2007 / Eckehard Schnieder;
		Géza Tarnai (Eds.) },
	publisher = { GZVB },
	pages = { 202-212 },
	year = { 2007 },
	address = { Braunschweig },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-188508 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/117067 },
}
[SSK07]
Schlich, B., Salewski, F., and Kowalewski, S., "Applying model checking to an automotive microcontroller application", in Proc. 2007 International Symposium on Industrial Embedded Systems : Costa da Caparica, [Lisbon], Portugal, 4 - 6 July 2007 ; [SIES'2007] / IEEE / IEEE Computer Society Press, Piscataway, NJ, 2007, IEEE, pp. 209-216.

Applying model checking to an automotive microcontroller application

Bibtex entry :

@inproceedings {  SSK07,
	author = { Schlich, Bastian and Salewski, Falk and Kowalewski, Stefan },
	title = { Applying model checking to an automotive microcontroller
		application },
	booktitle = { 2007 International Symposium on Industrial Embedded Systems
		: Costa da Caparica, [Lisbon], Portugal, 4 - 6 July 2007 ;
		[SIES'2007] / IEEE / IEEE Computer Society Press },
	publisher = { IEEE },
	pages = { 209-216 },
	year = { 2007 },
	address = { Piscataway, NJ },
	doi = { 10.1109/SIES.2007.4297337 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-188512 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/117071 },
}
[PSK06]
Palczynski, J., Schlich, B., and Kowalewski, S., "Eine Evaluationssuite zur schnellen Bewertung von Matlab/Simulink-Modelcheckern", in Proc. Informatik 2006 : Informatik für Menschen ; Beiträge der 36. Jahrestagung der Gesellschaft für Informatik e.V. (GI) ; 2. bis 6. Oktober 2006 in Dresden / Christian Hochberger ... (Hrsg.). - T. 1. - 1, Bonn, 2006 in GI-Edition : Proceedings, Ges. für Informatik, 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 },
	title = { Eine Evaluationssuite zur schnellen Bewertung von
		Matlab/Simulink-Modelcheckern },
	booktitle = { Informatik 2006 : Informatik f{\"u}r Menschen ; Beitr{\"a}ge
		der 36. Jahrestagung der Gesellschaft f{\"u}r Informatik
		e.V. (GI) ; 2. bis 6. Oktober 2006 in Dresden / Christian
		Hochberger ... (Hrsg.). - T. 1. - 1 },
	publisher = { Ges. f{\"u}r Informatik },
	pages = { 751-755 },
	series = { GI-Edition : Proceedings },
	year = { 2006 },
	address = { Bonn },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-183701 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/111754 },
}
[SK06a]
Schlich, B. and Kowalewski, S., "[mc]square: A model checker for microcontroller code", in Proc. ISoLA 2006 : Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation ; 15 - 19 November 2006, Paphos, Cyprus / IEEE Computer SocietyLeveraging 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 {  SK06a,
	author = { Schlich, Bastian and Kowalewski, Stefan },
	title = { [mc]square: A model checker for microcontroller code },
	booktitle = { ISoLA 2006 : Second International Symposium on Leveraging
		Applications of Formal Methods, Verification and Validation
		; 15 - 19 November 2006, Paphos, Cyprus / IEEE Computer
		SocietyLeveraging Applications of Formal Methods,
		Verification and Validation (ISoLA 2006) },
	publisher = { IEEE Computer Society Press },
	pages = { 466-473 },
	year = { 2006 },
	address = { Paphos, Cyprus },
	doi = { 10.1109/ISoLA.2006.62 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-188517 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/117076 },
}
[SRW+06]
Schlich, B., Rohrbach, M., Weber, M., and Kowalewski, S., "Model checking software for microcontrollers", , Aachen, AIB-2006-11, 2006.

Model checking software for microcontrollers

Bibtex entry :

@techreport {  SRW+06,
	author = { Schlich, Bastian and Rohrbach, Michael and Weber, Michael
		and Kowalewski, Stefan },
	title = { Model checking software for microcontrollers },
	pages = { 33 Bl. : graph. Darst. },
	volume = { 2006,11 },
	number = { AIB-2006-11 },
	series = { Aachener Informatik-Berichte },
	year = { 2006 },
	address = { Aachen },
	typ = { PUB:(DE-HGF)29 },
	reportid = { RWTH-CONV-008343 },
	cin = { 122810 / 120000 },
	url = { http://webdoc.sub.gwdg.de/ebook/serien/ah/AIB/2006-11.pdf },
}
[SK05b]
Schlich, B. and Kowalewski, S., "Model checking C source code for embedded systems", , [S.l.], NASA/CP-2005-212788, 2005.

Model checking C source code for embedded systems

Bibtex entry :

@techreport {  SK05b,
	author = { Schlich, Bastian and Kowalewski, Stefan },
	title = { Model checking C source code for embedded systems },
	booktitle = { IEEE/NASA Workshop on Leveraging Applications of Formal
		Methods, Verification, and Validation : IEEE/NASA ISoLA 2005
		; proceedings of a workshop held at the Loyola College
		Graduate Center, Columbia, Maryland, USA, 23 - 24 September
		2005 ; with a special track on the theme of formal methods
		in human and robotic space exploration / National
		Aeronautics and Space Administration, Goddard Space Flight
		Center. Ed.: Tiziana Margaria ... },
	pages = { 65-77 },
	number = { NASA/CP-2005-212788 },
	year = { 2005 },
	address = { [S.l.] },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-009447 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/111740 },
}
[SK04]
Schlich, B. and Kowalewski, S., "C Model Checker: Eine Übersicht", 2004.

C Model Checker: Eine Übersicht

Bibtex entry :

@inbook {  SK04,
	author = { Schlich, Bastian and Kowalewski, Stefan },
	title = { C Model Checker: Eine {\"U}bersicht },
	year = { 2004 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-101608 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/90178 },
}

Teaching

BSc/MSc/Diploma Theses

Lectures & Seminars


RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany