Dr.rer.nat. Bastian Schlich



Publikationen


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", 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.

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

Bibtex entry :

@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 },
}
[HBS+15]
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.

Analyzing the Restart Behavior of Industrial Control Applications

Bibtex entry :

@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 },
}
[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)7 },
	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 },
	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 },
}
[SBS+14]
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.

Applying Static Code Analysis on Industrial Controller Code

Bibtex entry :

@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 },
}
[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", 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.

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

Bibtex entry :

@inproceedings {  BKK+13,
	author = { Biallas, Sebastian and Kamin, Volker and Kowalewski, Stefan
		and Schlich, Bastian and Sehestedt, Stephan and Stattelmann,
		Stefan },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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.] },
	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 },
}
[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 },
	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 },
}
[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.] },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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.] },
	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 },
}
[SBW+09]
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

Direct Model Checking of PLC Programs in IL

Bibtex entry :

@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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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 },
	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 },
}
[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.] },
	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 },
}
[SK04]
Schlich, B. and Kowalewski, S., "C Model Checker: Eine Übersicht", 2004.

C Model Checker: Eine Übersicht

Bibtex entry :

@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 },
}
Diese Website verwendet Cookies. Durch die Nutzung der Website stimmen Sie dem Speichern von Cookies auf Ihrem Computer zu. Wenn Sie nicht einverstanden sind, verlassen Sie bitte die Website.Weitere Information

RWTH Aachen - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland