Dr.rer.nat. Bastian Schlich

Biallas, S., Simon, H., Kowalewski, S., Hauck-Stattelmann, S., and Schlich, B., "Automatische Testfallgenerierung für SPS-Programme mittels Zeilenüberdeckung", in Proc. Automation 2015 : 16. Branchentreff der Mess- und Automatisierungstechnik, 11. und 12. Juni 2015, Baden-Baden / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik, Düsseldorf, 2015 in VDI-Berichte, VDI-Verl., pp. 95-106.

@inproceedings {  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 : 16. Branchentreff der Mess- und
		Automatisierungstechnik, 11. und 12. Juni 2015, Baden-Baden
		/ VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik },
	publisher = { VDI-Verl. },
	pages = { 95-106 },
	series = { VDI-Berichte },
	year = { 2015 },
	address = { D{\"u}sseldorf },
	organization = { 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 },
}

Hauck-Stattelmann, S., Biallas, S., Schlich, B., Kowalewski, S., and Jetley, R., "Analyzing the Restart Behavior of Industrial Control Applications", in Proc. FM 2015: formal methods : 20th international symposium, Oslo, Norway, June 24 - 26, 2015 ; proceedings / Nikolaj Bjørner; Frank de Boer (eds.), Springer International Publishing, 2015 in Lecture Notes in Computer Science, Cham, pp. 585-588.

@inproceedings {  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 },
	series = { Lecture Notes in Computer Science },
	year = { 2015 },
	address = { Springer International Publishing },
	organization = { 20. 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)7 },
	reportid = { RWTH-CONV-207691 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/541096 },
}

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.

@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)7 },
	reportid = { RWTH-2015-07849 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/565382 },
}

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.

@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 },
	organization = { Discrete Event Systems : [12th International Workshop on
		Discrete Event Systems], Cachan (France), 2014-05-14 -
		2014-05-16 },
	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 },
}

Stattelmann, S., Biallas, S., Schlich, B., and Kowalewski, S., "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.

@inproceedings {  SBS+14,
	author = { Stattelmann, Stefan and Biallas, Sebastian and Schlich,
		Bastian and Kowalewski, Stefan },
	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 },
}

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 : 14. Branchentreff der Mess- und Automatisierungstechnik ; Kongresshaus Baden-Baden, 25. und 26. Juni 2013 / VDI/VDE-Gesellschaft Mess- und Automatisierungstechnik, Düsseldorf, 2013 in VDI-Berichte, VDI-Verl., pp. 75-79.

@inproceedings {  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 },
	series = { VDI-Berichte },
	year = { 2013 },
	address = { D{\"u}sseldorf },
	organization = { 14. Branchentreff der Mess- und Automatisierungstechnik
		(Germany), 2013-06-25 - 2013-06-26 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-203699 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/226206 },
}

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.

@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 },
	organization = { 13. Branchentreff der Mess- und Automatisierungstechnik,
		Baden-Baden (Germany), 2011-06-13 - 2011-06-14 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-191631 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/120638 },
}

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

@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 },
}

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.

@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 },
}

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

@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 },
	organization = { 4. International Workshop on Numerical and Symbolic Abstract
		Domains (France), 10-09-2010 },
	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 },
}

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.

@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.] },
	organization = { Formal methods for automation and safety in railway and
		automotive systems, 2010 },
	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 },
}

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.

@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 },
	organization = { 12. Branchentreff der Mess- und Automatisierungstechnik,
		Baden-Baden (Germany), 2011-06-28 - 2011-06-29 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-189475 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/118212 },
}

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

@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 },
}

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

@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 },
}

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.

@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.] },
	organization = { 5. International Haifa Verification Conference, HCV 2009,
		Haifa (Israel), 2009-10-19 - 2009-10-22 },
	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 },
}

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.

@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 },
	organization = { Entwurf komplexer Automatisierungssysteme :
		Beschreibungsmittel, Methoden, Werkzeuge und Anwendungen,
		Magdeburg (Germany), 2010-05-25 - 2010-05-27 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190099 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/118924 },
}

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.

@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 },
	organization = { 13. International Workshop on Software & Compilers for
		Embedded Systems, St. Goar (Germany), 2010-06-29 -
		2010-06-30 },
	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 },
}

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.

@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 },
	organization = { 13. IEEE Symposium on Design and Diagnostics of Electronic
		Circuits and Systems, Vienna (Austria), 2010-04-14 -
		2010-04-16 },
	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 },
}

Schlich, B., "Model Checking of Software for Microcontrollers", ACM transactions on embedded computing systems : TECS, vol. 9, iss. 4, p. 27, 2010

@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 },
}

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

@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 },
}

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.

@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 },
	organization = { 2009 international conference on Compilers, architecture,
		and synthesis for embedded systems, Grenoble (France),
		2009-10-11 - 2009-10-16 },
	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 },
}

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.

@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 },
}

Klein, G., Huuck, R., and Schlich, B., "Operating System Verification", Journal of automated reasoning, vol. 42, iss. 2/4, pp. 123-124, 2009

@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 },
}

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.

@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 },
	organization = { 2009 IEEE International Symposium on Industrial Embedded
		Systems, Lausanne (Switzerland), 2009-07-08 - 2009-07-10 },
	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 },
}

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.

@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 },
	organization = { 2009 Fourth International Conference on Embedded and
		Multimedia Computing, Jeju Island (South Korea), 2009-12-10
		- 2009-12-12 },
	doi = { 10.1109/EM-COM.2009.5402986 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-199048 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/129021 },
}

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.

@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.] },
	organization = { 2009 IEEE Symposium on Design and Diagnostics of Electronic
		Circuits and Systems, Liberec (Czech Republic), 2009-04-15 -
		2009-04-17 },
	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 },
}

Schlich, B., Brauer, J., Wernerus, J., and Kowalewski, S., "Direct Model Checking of PLC Programs in IL", IFAC Proceedings Volumes, vol. 42, iss. 5, pp. 28-33, 2009

@article {  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 },
	journal = { IFAC Proceedings Volumes },
	publisher = { Elsevier },
	pages = { 28-33 },
	volume = { 42 },
	number = { 5 },
	year = { 2009 },
	address = { Amsterdam },
	issn = { 1474-6670 },
	isbn = { 978-3-902661-44-9 },
	organization = { 2. IFAC Workshop on Dependable Control of Discrete Systems,
		Bari (Italy), 2009-06-10 - 2009-06-12 },
	doi = { 10.3182/20090610-3-IT-4004.00010 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-236337 },
	cin = { 122810 / 120000 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:SBWK09.pdf },
}

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

@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 },
}

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.

@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 },
	organization = { 10. Branchentreff der Mess- und Automatisierungstechnik,
		Baden-Baden (Germany), 2009-06-16 - 2009-06-17 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-172091 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/99088 },
}

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.

@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 },
}

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

@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 },
}

Noll, T. and Schlich, B., "Delayed nondeterminism in model checking embedded systems assembly code"Berlin [u.a.]: Springer, 2008, vol. 4899, pp. 185-201.

@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 },
}

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.

@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 },
	organization = { 2008 IEEE/ASME International Conference on Mechatronic and
		Embedded Systems and Applications, Beijing (Peoples R
		China), 2008-10-12 - 2008-10-15 },
	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 },
}

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.

@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 },
	organization = { 2008 International Symposium on Industrial Embedded Systems,
		La Grande Motte (France), 2008-06-11 - 2008-06-13 },
	doi = { 10.1109/SIES.2008.4577709 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-172528 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/99569 },
}

Schlich, B., "Model checking of software for microcontrollers", PhD Thesis, Aachen, 2008.

@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 },
}

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.

@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 },
	organization = { Symposium FORMS/FORMAT 2008, Budapest (Hungary), 2008-10-09
		- 2008-10-10 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-171805 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/98749 },
}

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.

@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 },
}

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.

@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 },
	organization = { 6. symposium : formal methods for automation and safety in
		railway and automotive systems, Braunschweig (Germany),
		2007-01-25 - 2007-01-26 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-188508 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/117067 },
}

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.

@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 },
	organization = { International Symposium on Industrial Embedded Systems,
		Costa da Caparica (Portugal), 2007-07-04 - 2007-07-06 },
	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 },
}

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.

@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 },
	organization = { 36. Jahrestagung der Gesellschaft f{\"u}r Informatik e.V.,
		Dresden (Germany), 2006-10-02 - 2006-10-06 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-183701 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/111754 },
}

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.

@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 },
	organization = { 2. International Symposium on Leveraging Applications of
		Formal Methods, Verification and Validation, Paphos
		(Cyprus), 2006-11-15 - 2006-11-19 },
	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 },
}

Schlich, B., Rohrbach, M., Weber, M., and Kowalewski, S., "Model checking software for microcontrollers", , Aachen, AIB-2006-11, 2006.

@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 },
}

Schlich, B. and Kowalewski, S., "Model checking C source code for embedded systems", , [S.l.], NASA/CP-2005-212788, 2005.

@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.] },
	organization = { IEEE/NASA Workshop on Leveraging Applications of Formal
		Methods, Verification, and Validation, Columbia (USA),
		2005-09-23 - 2005-09-24 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-009447 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/111740 },
}

Schlich, B. and Kowalewski, S., "C Model Checker: Eine Übersicht", 2004.

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