Dr.rer.nat. Bastian Schlich

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

Ich war von April 2004 bis Februar 2010 erst als Doktorand und danach als Postdoc am Lehrstuhl Informatik 11 (Software für eingebettete Systeme) beschäftigt. An diesem Lehrstuhl leitete ich die Gruppe Formale Verifikation. Mein Forschungsschwerpunkt war die formale Verifikation von Software für eingebettete Systeme. Unter formaler Verifikation verstehe ich die Anwendung von Methoden wie z. B. statische Analyse, abstrakte Interpretation und Model-Checking.

Die Gruppe arbeitet an einem Werkzeug zur Analyse von Assembler-Code für Mikrocontroller und AWL-Programmen für SPSen. Das Werkzeug heißt [mc]square. In diesem Werkezug werden unterschiedliche formale Methoden kombiniert und an die Gegebenheiten von eingebetteten Systemen angepasst. Das Hauptaugenmerk hierbei liegt auf der Anwendung theoretischer Resultate auf reale Probleme. Das Werkzeug soll möglichst leicht zu benutzen sein und keine Änderungen an den zu verifizierenden Programmen benötigen.

In einem weiteren Projekt wird ein Werkezug für die statische Analyse von C Code entwickelt, welches die Entwicklung von eingebetteter Software anhand des bevorstehenden ISO Standards ISO 26262 unterstützen soll. Es wird zuerst ein Plugin für die Eclipse Entwicklungsumgebung erstellt. Später wird auch ein Plugin für die Microsoft Visual Studio Entwicklungsumgebung implementiert.

Meinen Doktortitel habe ich im Juni 2008 von der RWTH Aachen erhalten. Der Titel meiner Dissertation lautet „Model Checking of Software for Microcontrollers“. Meine Diplomarbeit habe ich am Lehrstuhl für Software-Technologie der Universität Dortmund geschrieben. Der Titel meiner Diplomarbeit ist „Konzeption und Realisierung eines Werkzeugs zur Unterstützung der Test-Driven-Developments“.

[SBK10]

PDF   BIB

B. Schlich, J. Brauer, and S. Kowalewski, "Application of Static Analyses for State Space Reduction to Microcontroller Binary Code", Science of Computer Programming: Special Issue on FMICS 2007 & 2008, 2010, To appear

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

Bibtex entry :

@article { SBK10,
    author = { Schlich, Bastian and Brauer, J{\"o}rg and Kowalewski, Stefan },
    title = { Application of Static Analyses for State Space Reduction to
		Microcontroller Binary Code },
    journal = { Science of Computer Programming: Special Issue on FMICS 2007
		& 2008 },
    year = { 2010 },
    note = { To appear },
}

[RHS+09]

PDF   BIB

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

Model Checking Assembly Code of an Industrial Knitting Machine

Bibtex entry :

@inproceedings { RHS+09,
    author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian
		and Brauer, J{\"o}rg and Scheuer, Florian },
    title = { Model Checking Assembly Code of an Industrial Knitting
		Machine },
    booktitle = { Embedded and Multimedia Computing (EM-Com 2009), Jeju, Korea },
    year = { 2009 },
    publisher = { IEEE Computer Society Press },
    note = { To appear },
}

[SBWK09]

PDF   BIB

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

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

Bibtex entry :

@inproceedings { SBWK09,
    author = { Schlich, Bastian and Brauer, J{\"o}rg and Wernerus, J{\"o}rg
		and  Kowalewski, Stefan },
    booktitle = { Dependable Control of Discrete Systems (DCDS'09), Bari,
		Italy },
    note = { To appear },
    title = { Direct Model Checking of {PLC} Programs in {IL} },
    year = { 2009 },
}

[RHS09]

PDF   BIB

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

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

Bibtex entry :

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

[Sch09]

PDF   BIB

B. Schlich, "Model Checking of Software for Microcontrollers", ACM Transactions in Embedded Computing Systems (TECS), 2009, To appear

Model Checking of Software for Microcontrollers

Bibtex entry :

@article { Sch09,
    author = { Schlich, Bastian },
    journal = { ACM Transactions in Embedded Computing Systems (TECS) },
    note = { To appear },
    publisher = { ACM Press },
    title = { Model Checking of Software for Microcontrollers },
    year = { 2009 },
}

[SK09]

PDF   BIB

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

Model Checking {C} Source Code for Embedded Systems

Bibtex entry :

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

[SKW09]

PDF   BIB

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

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

Bibtex entry :

@inproceedings { SKW09,
    address = { D{\"u}sseldorf },
    author = { Schlich, Bastian and Kowalewski, Stefan and Wernerus,
		J{\"o}rg },
    booktitle = { AUTOMATION 2009, Baden-Baden, Germany },
    isbn = { 978-3-18-092067-2 },
    number = { 2067 },
    publisher = { VDI Verlag },
    series = { VDI-Berichte },
    title = { {Verifikation von SPS-Programmen in AWL mit Hilfe von
		direktem Model-Checking} },
    year = { 2009 },
}

[SNBB09]

PDF   BIB

B. Schlich, T. Noll, J. Brauer, and L. Brutschy, "Reduction of Interrupt Handler Executions for Model Checking Embedded Software", in Proc. Haifa Verification Conference (HVC 2009), Haifa, Israel, 2009, To appear.

Reduction of Interrupt Handler Executions for Model Checking Embedded Software

Bibtex entry :

@inproceedings { SNBB09,
    author = { Schlich, B. and Noll, T. and Brauer, J. and Brutschy, L. },
    title = { Reduction of Interrupt Handler Executions for Model Checking
		Embedded Software },
    booktitle = { Haifa Verification Conference (HVC 2009), Haifa, Israel },
    year = { 2009 },
    note = { To appear },
}

[RBHS09]

PDF   BIB

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

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

Bibtex entry :

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

[BSK09b]

PDF   BIB

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

Parallel and Distributed Invariant Checking of Microcontroller Software

Bibtex entry :

@article { BSK09b,
    title = { Parallel and Distributed Invariant Checking of
		Microcontroller Software },
    journal = { Electronic Notes in Theoretical Computer Science },
    volume = { 254 },
    pages = { 45–63 },
    year = { 2009 },
    note = { Proceedings of the 4th International Workshop on Systems
		Software Verification (SSV 2009) },
    publisher = { Elsevier },
    issn = { 1571-0661 },
    author = { Brauer, J{\”o}rg and Schlich, Bastian and Kowalewski,
		Stefan },
}

[BHS09]

PDF   BIB

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

Interprocedural Pointer Analysis in Goanna

Bibtex entry :

@article { BHS09,
    author = { Brauer, J{\"o}rg and Huuck, Ralf and Schlich, Bastian },
    title = { Interprocedural Pointer Analysis in Goanna },
    journal = { Electronic Notes in Theoretical Computer Science },
    volume = { 254 },
    pages = { 65–83 },
    year = { 2009 },
    note = { Proceedings of the 4th International Workshop on Systems
		Software Verification (SSV 2009) },
    publisher = { Elsevier },
    issn = { 1571-0661 },
}

[BSRK09]

PDF   BIB

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

Stack Bounds Analysis of Microcontroller Assembly Code

Bibtex entry :

@inproceedings { BSRK09,
    author = { Brauer, J{\"o}rg and Schlich, Bastian and Reinbacher, Thomas
		and Kowalewski, Stefan },
    title = { Stack Bounds Analysis of Microcontroller Assembly Code },
    booktitle = { Workshop on Embedded Security (WESS 2009), Grenoble, France },
    year = { 2009 },
    publisher = { ACM Press },
}

[FHST09]

PDF   BIB

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

Automatic Bug Detection in Microcontroller Software by Static Program Analysis

Bibtex entry :

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

[SGK08]

PDF   BIB

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

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

Bibtex entry :

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

[Sch08]

PDF   BIB

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

Model Checking of Software for Microcontrollers

Bibtex entry :

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

[RKHS08b]

PDF   BIB

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

Motivating Model Checking for Embedded Systems Software

Bibtex entry :

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

[SLK08]

PDF   BIB

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

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

Bibtex entry :

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

[BKKS08]

PDF   BIB

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

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

Bibtex entry :

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

[RKHS08a]

PDF   BIB

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

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

Bibtex entry :

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

[HNSW08]

PDF   BIB

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

Proving Correctness of an Efficient Abstraction for Interrupt Handling

Bibtex entry :

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

[NS08]

PDF   BIB

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

Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code

Bibtex entry :

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

[SK07f]

PDF   BIB

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

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

Bibtex entry :

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

[SSK07]

PDF   BIB

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

Applying Model Checking to an Automotive Microcontroller Application

Bibtex entry :

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

[SK06b]

PDF   BIB

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

[mc]square: A model checker for microcontroller code

Bibtex entry :

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

[SRWK06]

PDF   BIB

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

Model Checking Software for Microcontrollers

Bibtex entry :

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

[PSK06]

PDF   BIB

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

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

Bibtex entry :

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

[SK05]

PDF   BIB

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

Model Checking {C} Source Code for Embedded Systems

Bibtex entry :

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

[SK04]

PDF   BIB

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

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

Bibtex entry :

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

• Gegenbeispiel-geleitete Abstraktionsverfeinerung für speicherprogrammierbare Steuerungen (Sebastian Biallas)
• Erweiterung von EVA für 16 und 32 Bit Systeme (Michael Lambertz)
• Statische Analyse für den Renesas R8C/23 Mikrocontroller (Jörg Toborg)
• Statische Analyse von Mikrocontrollerprogrammen mittels SAT- und Constraint-Solving (Lucas Brutschy)
• Implementierung eines Simulators für Renesas-Mikrocontroller (Mudassir Rasool)
• Synthese eines Befehlssatz-Simulators für das Model-Checking von Software für eingebettete Systeme (Ivica Bogosavljevic)
• Model-Checking von Anweisungslisten-Programmen für Speicherprogrammierbare Steuerung mit Hilfe von [mc]square (Jörg Wernerus)
• Paralleler und verteilter Aufbau des Zustandsraums im Model-Checker [mc]square (Stefan Mau)
• Erweiterung der symbolischen Zustandsdarstellung in [mc]square (Dipl.-Inform. Volker Kamin)
• Model-Checking von Sensornetzwerk-Knoten mit Hilfe von [mc]square (Matthias Moers)
• Erweiterung des Model-Checkers [mc]square um benutzerdefinierte Umgebungen (Dipl.-Inform. Dominique Marcel Gückel)
• Erweiterung des Model-Checkers [mc]square für den Infineon XC167 Mikrocontroller (Florian Scheuer)
• Einsatz von statischen Analysen im Bereich des Model-Checking von Software für eingebettete Systeme (Jann Löll)
• Symbolisches Model-Checking mit [mc]square (Dipl.-Inform. John F. Schommer)
• Ein Ansatz zum Model-Checking von Software für eingebettete Systeme (Michael Rohrbach)
• Untersuchungen zum Anwendungspotenzial der formalen Verifikation im Bereich Motorsteuerungssoftware (Dipl.-Inform. Andreas Polzer)
• Anforderungen an einen Modelchecker für Matlab/Simulink (Dipl.-Inform. Jacob Palczynski)

• Wintersemester 09/10: Formale Methoden für eingebettete Systeme (Vorlesung)
• Sommersemester 09: Anwendung formaler Verifikationsmethoden auf eingebettete Systeme (Seminar)
• Wintersemester 08/09: Statische Analyse von Software für eingebettete Systeme (Seminar)
• Sommersemester 08: Formale Methoden für eingebettete Systeme (Vorlesung)
• Sommersemester 07: Formale Methoden für eingebettete Systeme (Vorlesung)
• Wintersemester 06/07: Testen von eingebetteten Systemen (Seminar)
• Sommersemester 06: SUN Softwarepreis 2006
• Wintersemester 05/06: Systematische Software-Entwicklung (Vorlesung)
• Sommersemester 05: Formale Methoden für eingebettete Systems (Vorlesung)
• Wintersemester 04/05: Systemprogrammierung (Vorlesung)
• Wintersemester 04/05: Anwendung von Model-Checking auf eingebettete Systeme (Seminar)
• Sommersemester 04: Hybride und Echtzeitsysteme (Seminar)