Dies ist eine alte Version des Dokuments!
I am a research assistant at the embedded software laboratory since April 2004. My research topic is the formal verification of software for embedded systems.
At present I am working on a model checker for microcontroller code. It is called [mc]square. The main focus is the application of theoretical results to real problems. The model checker should be as user-friendly as possible and the need for manual preparation of the code should be as small as possible. In the tool, we combine different formal methods such as model checking, abstract interpretation, and static analysis.
I received my Doctoral degree in June 2008 from the RWTH Aachen University. The title of my Dissertation thesis is „Model Checking of Software for Microcontollers“. I wrote my Diploma thesis at the chair of Software-Technology, University of Dortmund. The topic of the thesis is „Konzeption und Realisierung eines Werkzeugs zur Unterstützung des Test-Driven-Developments“.
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
@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 }, }
(Dipl.-Inform. John F. Schommer)