Publications

Biallas, S., Brauer, J., and Kowalewski, "SAT-Based Abstraction Refinement for Programmable Logic Controllers", in Proc. Dependable Control of Discrete Systems (DCDS 2011), 2011, To appear.

@inproceedings { BBK11,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski },
	title = { SAT-Based Abstraction Refinement for Programmable Logic
		Controllers },
	booktitle = { Dependable Control of Discrete Systems (DCDS 2011) },
	i11key = { conference },
	year = { 2011 },
	timestamp = { 2011.03.15 },
	note = { To appear },
}

Brauer, J. and King, A., "Transfer Function Synthesis without Quantifier Elimination", in Proc. European Symposium on Programming (ESOP 2011), 2011, vol. 6602 in Lecture Notes in Computer Science, Springer, pp. 97-115.

@inproceedings { BK11a,
	author = { Brauer, J{\"o}rg and King, Andy },
	title = { Transfer Function Synthesis without Quantifier Elimination },
	booktitle = { European Symposium on Programming (ESOP 2011) },
	i11key = { conference },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	pages = { 97--115 },
	volume = { 6602 },
	timestamp = { 2010.12.07 },
	year = { 2011 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bk11.pdf },
}

Schlich, B., Brauer, J., and Kowalewski, S., "Application of Static Analyses for State Space Reduction to Microcontroller Binary Code", Sci. Comput. Program., vol. 76, iss. 2, pp. 100-118, 2011

@article { SBK11,
	author = { Schlich, Bastian and Brauer, J{\"o}rg and Kowalewski, Stefan },
	title = { Application of Static Analyses for State Space Reduction to
		Microcontroller Binary Code },
	journal = { Sci. Comput. Program. },
	year = { 2011 },
	volume = { 76 },
	number = { 2 },
	pages = { 100--118 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:sbk10.pdf },
	i11key = { journal },
	timestamp = { 2010.12.06 },
}

Biallas, S., Brauer, J., and Kowalewski, S., "Counterexample-Guided Abstraction Refinement for PLCs", in Proc. 5th International Workshop on Systems Software Verification (SSV 2010), Vancouver, Canada, 2010, To appear.

@inproceedings { BBK10,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
		Stefan },
	title = { Counterexample-Guided Abstraction Refinement for PLCs },
	booktitle = { 5th International Workshop on Systems Software Verification
		(SSV 2010), Vancouver, Canada },
	year = { 2010 },
	timestamp = { 2010.07.19 },
	note = { To appear },
	i11key = { conference },
}

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. Tagungsband Entwicklung und Betrieb komplexer Automatisierungssysteme (EKA 2010), 2010, To appear.

@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 = { Tagungsband Entwicklung und Betrieb komplexer
		Automatisierungssysteme (EKA 2010) },
	year = { 2010 },
	location = { Magdeburg, Germany },
	note = { To appear },
}

Brauer, J. and King, A., "Automatic Abstraction for Intervals using Boolean Formulae", in Proc. Static Analysis Symposium (SAS 2010), Perpignan, France, 2010 in Lecture Notes in Computer Science, Springer, To appear.

@inproceedings { BK10,
	author = { Brauer, J{\"o}rg and King, Andy },
	title = { Automatic Abstraction for Intervals using Boolean Formulae },
	booktitle = { Static Analysis Symposium (SAS 2010), Perpignan, France },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	year = { 2010 },
	timestamp = { 2010.05.04 },
	note = { To appear },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bk10.pdf },
	i11key = { conference },
}

Brauer, J., King, A., and Kowalewski, S., "Range Analysis of Microcontroller Code using Bit-Level Congruences", in Proc. Formal Methods for Industrial Critical Systems (FMICS 2010), Antwerp, Belgium, 2010, vol. 6371 in Lecture Notes in Computer Science, Springer, pp. 82-98, To appear.

@inproceedings { BKK10,
	author = { Brauer, J{\"o}rg and King, Andy and Kowalewski, Stefan },
	title = { Range Analysis of Microcontroller Code using Bit-Level
		Congruences },
	booktitle = { Formal Methods for Industrial Critical Systems (FMICS 2010),
		Antwerp, Belgium },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	year = { 2010 },
	volume = { 6371 },
	pages = { 82--98 },
	timestamp = { 2010.06.08 },
	note = { To appear },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bkk10.pdf },
	i11key = { conference },
}

Brauer, J., Kamin, V., Kowalewski, S., and Noll, T., "Loop Refinement using Octagons and Satisfiability", in Proc. 5th International Workshop on Systems Software Verification (SSV 2010), Vancouver, Canada, 2010, To appear.

@inproceedings { BKKN10,
	author = { Brauer, J{\"o}rg and Kamin, Volker and Kowalewski, Stefan
		and Noll, Thomas },
	title = { Loop Refinement using Octagons and Satisfiability },
	booktitle = { 5th International Workshop on Systems Software Verification
		(SSV 2010), Vancouver, Canada },
	year = { 2010 },
	timestamp = { 2010.07.19 },
	note = { To appear },
	i11key = { conference },
}

Brauer, J., Noll, T., and Schlich, B., "Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software", in Proc. Proceedings of the 13th International Workshop on Software and Compilers for Embedded Systems (SCOPES 2010), 2010, ACM, To appear.

@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 = { Proceedings of the 13th International Workshop on Software
		and Compilers for Embedded Systems (SCOPES 2010) },
	year = { 2010 },
	note = { To appear },
	publisher = { ACM },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:BNS10.pdf },
	timestamp = { 2010.04.01 },
	i11key = { conference },
}

Gückel, D., Brauer, J., and Kowalewski, S., "A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification", in Proc. Industrial Embedded Systems (SIES 2010), Trento, Italy, 2010, To appear.

@inproceedings { GBK10,
	author = { G{\"u}ckel, Dominique and Brauer, J{\"o}rg and Kowalewski,
		Stefan },
	booktitle = { Industrial Embedded Systems (SIES 2010), Trento, Italy },
	title = { A System for Synthesizing Abstraction-Enabled Simulators for
		Binary Code Verification },
	year = { 2010 },
	note = { To appear },
	timestamp = { 2010.06.01 },
	i11key = { conference },
}

Gückel, D., Schlich, B., Brauer, J., and Kowalewski, S., "Synthesizing Simulators for Model Checking Microcontroller Binary Code", in Proc. Proceedings of the 13th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2010), 2010, To appear.

@inproceedings { GSBK10,
	author = { G{\"u}ckel, Dominique and Schlich, Bastian and Brauer,
		J{\"o}rg and Kowalewski, Stefan },
	title = { Synthesizing Simulators for Model Checking Microcontroller
		Binary Code },
	booktitle = { Proceedings of the 13th IEEE International Symposium on
		Design and Diagnostics of Electronic Circuits and Systems
		(DDECS 2010) },
	year = { 2010 },
	note = { To appear },
	owner = { gueckel },
	i11key = { conference },
	timestamp = { 2010.03.08 },
}

Brauer, J., Schlich, B., and Kowalewski, S., "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)

@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 },
	url = { http://portal.acm.org/citation.cfm?id=1630177.1630457 },
	i11key = { conference },
}

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

@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 },
	url = { http://portal.acm.org/citation.cfm?id=1631716.1631721 },
	i11key = { conference },
}

Fehnker, A., Huuck, R., Schlich, B., and Tapp, M., "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, vol. 5404 in Lecture Notes in Computer Science, Springer, pp. 267-278.

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

Gückel, D., "Retargeting a Hardware-Dependent Model Checker by Using Architecture Description Languages", in Proc. Doctoral Symposium on Systems Software Verification (DS SSV 2009), 2009 in Aachener Informatik-Berichte.

@inproceedings { Guec09,
	author = { G{\"u}ckel, Dominique },
	title = { Retargeting a Hardware-Dependent Model Checker by Using
		Architecture Description Languages },
	booktitle = { Doctoral Symposium on Systems Software Verification (DS SSV
		2009) },
	issn = { 0935–3232 },
	year = { 2009 },
	series = { Aachener Informatik-Berichte },
	owner = { gueckel },
	timestamp = { 2009.06.02 },
	url = { http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2009/2009-14.pdf },
}

Klünder, D., "Entwurf eingebetteter Software mit abstrakten Zustandsmaschinen und Business Object Notation", RWTH Aachen University, AIB-2009-04, 2009.

@techreport { Klu09,
	author = { Daniel Kl{\"u}nder },
	title = { Entwurf eingebetteter Software mit abstrakten
		Zustandsmaschinen und Business Object Notation },
	institution = { RWTH Aachen University },
	year = { 2009 },
	number = { AIB-2009-04 },
	month = { feb },
	url = { http://aib.informatik.rwth-aachen.de/2009/2009-04.pdf },
	issn = { 0935-3232 },
}

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

@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 },
	url = { http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5196212 },
	i11key = { conference },
}

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

@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 },
	i11key = { conference },
}

Reinbacher, T., Horauer, M., and Schlich, B., "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, IEEE Computer Society Press, pp. 114-119.

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

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

@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 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:SBWK09.pdf },
	i11key = { conference },
}

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

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

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

@article { SK09,
	author = { Schlich, Bastian and Kowalewski, Stefan },
	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 },
}

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

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

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

@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 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:SNBB09.pdf },
	note = { To appear },
	i11key = { conference },
}

Thomas, W., Bollue, K., Gückel, D., Quiros, G., Slaats, M., and Ummels, M., "DFG Research Training Group "Algorithmic Synthesis of Reactive and Discrete-Continuous Systems (AlgoSyn)"", it - Information Technology, vol. 4, pp. 222-230, 2009

@article { TBG+09,
	author = { Thomas, Wolfgang and Bollue, Kai and G{\"u}ckel, Dominique
		and Quiros, Gustavo and Slaats, Michaela and Ummels, Michael },
	title = { DFG Research Training Group "Algorithmic Synthesis of
		Reactive and Discrete-Continuous Systems (AlgoSyn)" },
	journal = { it - Information Technology },
	year = { 2009 },
	volume = { 4 },
	pages = { 222-230 },
	owner = { gueckel },
	timestamp = { 2009.05.25 },
}

Beckers, J., Klünder, D., Kowalewski, S., and Schlich, B., "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, vol. 5238 in Lecture Notes in Computer Science, Springer, pp. 112-124.

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

Huuck, R., Fehnker, A., Seefried, S., and Brauer, J., "Goanna: Syntactic Software Model Checking", in Proc. Automated Technology for Verification and Analysis (ATVA 2008), Seoul, Korea, 2008, vol. 5311 in Lecture Notes in Computer Science, Springer, pp. 216-221.

@inproceedings { HFSB08,
	author = { Huuck, Ralf and Fehnker, Ansgar and Seefried, Sean and
		Brauer, J{\"o}rg },
	bibsource = { DBLP, http://dblp.uni-trier.de },
	booktitle = { Automated Technology for Verification and Analysis (ATVA
		2008), Seoul,  Korea },
	doi = { 10.1007/978-3-540-88387-6 },
	ee = { http://dx.doi.org/10.1007/978-3-540-88387-6_17 },
	isbn = { 978-3-540-88386-9 },
	pages = { 216-221 },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	title = { Goanna: Syntactic Software Model Checking },
	volume = { 5311 },
	year = { 2008 },
	bdsk-url-1 = { http://dx.doi.org/10.1007/978-3-540-88387-6 },
	url = { http://www.springerlink.com/content/7h567h368nt7v719/ },
	i11key = { conference },
}

Herberich, G., Noll, T., Schlich, B., and Weise, C., "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)

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

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

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

Reinbacher, T., Kramer, M., Horauer, M., and Schlich, B., "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, IEEE Computer Society Press, pp. 245-248.

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

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

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

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

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

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 (FORMS/FORMAT 2008), Budapest, Hungary, Budapest, Hungary, 2008, L'Harmattan, pp. 27-34.

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

Schlich, B., Löll, J., and Kowalewski, S., "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, vol. 4916 in Lecture Notes in Computer Science, Springer, pp. 21-37.

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

Schlich, B. and Kowalewski, S., "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, GZVB, pp. 202-212.

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

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

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

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

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

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

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

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

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

Schlich, B. and Kowalewski, S., "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, NASA, pp. 65-77, NASA/CP-2005-212788.

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

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

@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} },
	year = { 2004 },
}

Brauer, J. and King, A., "Approximate Quantifier Elimination for Propositional Boolean Formulae", in Proc. NASA Formal Methods Symposium (NFM 2011), , vol. 6617 in Lecture Notes in Computer Science, Springer, pp. 73-88.

@inproceedings { BK11b,
	author = { Brauer, J{\"o}rg and King, Andy },
	title = { Approximate Quantifier Elimination for Propositional Boolean
		Formulae },
	booktitle = { NASA Formal Methods Symposium (NFM 2011) },
	i11key = { conference },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	pages = { 73--88 },
	volume = { 6617 },
	timestamp = { 2011.03.04 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bk11b.pdf },
}