Publications

Grochowski, M., Simon, H., Bohlender, D., Kowalewski, S., Löcklin, A., Müller, T., Jazdi, N., Zeller, A., and Weyrich, M., "Formale Methoden für rekonfigurierbare cyber-physische Systeme in der Produktion", Automatisierungstechnik, vol. 68, iss. 1, pp. 3-14, 2020

@article { GSB+20,
	author = { Grochowski, Marco and Simon, Hendrik and Bohlender, Dimitri
		and Kowalewski, Stefan and L{\"o}cklin, Andreas and
		M{\"u}ller, Timo and Jazdi, Nasser and Zeller, Andreas and
		Weyrich, Michael },
	title = { Formale Methoden f{\"u}r rekonfigurierbare cyber-physische
		Systeme in der Produktion },
	journal = { Automatisierungstechnik },
	publisher = { De Gruyter },
	pages = { 3-14 },
	volume = { 68 },
	number = { 1 },
	year = { 2020 },
	address = { Berlin },
	issn = { 2196-677X },
	doi = { 10.1515/auto-2019-0115 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-2019-12214 },
	cin = { 122810 / 120000 },
	url = { https://www.degruyter.com/view/j/auto.2020.68.issue-1/auto-2019-0115/auto-2019-0115.xml },
}

Bohlender, D. and Kowalewski, S., "Leveraging Horn clause solving for compositional verification of PLC software", Discrete event dynamic systems, vol. 30, pp. 1-24, 2019

@article { BK19,
	author = { Bohlender, Dimitri and Kowalewski, Stefan },
	title = { Leveraging Horn clause solving for compositional
		verification of PLC software },
	journal = { Discrete event dynamic systems },
	publisher = { Springer Science + Business Media B.V },
	pages = { 1-24 },
	volume = { 30 },
	year = { 2019 },
	address = { Dordrecht [u.a.] },
	issn = { 0924-6703 },
	doi = { 10.1007/s10626-019-00296-8 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-2019-12207 },
	cin = { 122810 / 120000 },
}

Bohlender, D. and Kowalewski, S., "Design and Verification of Restart-robust Industrial Control Software", in Proc. Integrated Formal Methods - 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, 2018, Springer, pp. 47-68.

@inproceedings { BK18a,
	author = { Bohlender, Dimitri and Kowalewski, Stefan },
	title = { Design and Verification of Restart-robust Industrial Control
		Software },
	booktitle = { Integrated Formal Methods - 14th International Conference,
		IFM 2018, Maynooth, Ireland, September 5-7, 2018 },
	publisher = { Springer },
	publishedas = { Druck Online },
	isbn = { 978-3-319-98938-9 },
	language = { eng },
	pages = { 47--68 },
	year = { 2018 },
	timestamp = { 2018.06.18 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2018 },
}

Simon, H., Triefenbach, L., and Kowalewski, S., "Structural Concolic Testing fpr Sequential Function Chart", in Proc. 14th International Workshop on Discrete Event Systems, WODES 2018, Sorrento Coast, Italy, May 30 - June 1, 2018, 2018, vol. 51, Elsevier, pp. 422-427.

@inproceedings { STK18,
	author = { Simon, Hendrik and Triefenbach, Lucas and Kowalewski, Stefan },
	editor = { Gianmaria De Tommasi },
	title = { Structural Concolic Testing fpr Sequential Function Chart },
	booktitle = { 14th International Workshop on Discrete Event Systems, WODES
		2018, Sorrento Coast, Italy, May 30 - June 1, 2018 },
	volume = { 51 },
	publisher = { Elsevier },
	publishedas = { Online },
	issn = { 2405-8963 },
	language = { eng },
	pages = { 422--427 },
	year = { 2018 },
	timestamp = { 2018.06.06 },
	i11key = { conference },
	i11projectkey = { Arcade },
	url = { https://www.sciencedirect.com/journal/ifac-papersonline/vol/51/issue/7 },
	for_reporting_period = { 2018 },
}

Bohlender, D. and Kowalewski, S., "Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction", in Proc. 14th International Workshop on Discrete Event Systems, WODES 2018, Sorrento Coast, Italy, May 30 - June 1, 2018, 2018, IFAC, pp. 428-433.

@inproceedings { BK18,
	author = { Bohlender, Dimitri and Kowalewski, Stefan },
	title = { Compositional Verification of PLC Software using Horn
		Clauses and Mode Abstraction },
	booktitle = { 14th International Workshop on Discrete Event Systems, WODES
		2018, Sorrento Coast, Italy, May 30 - June 1, 2018 },
	publisher = { IFAC },
	publishedas = { Online },
	issn = { 2405-8963 },
	language = { eng },
	pages = { 428--433 },
	year = { 2018 },
	timestamp = { 2018.03.05 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2018 },
}

Bohlender, D., Hamm, D., and Kowalewski, S., "Cycle-Bounded Model Checking of PLC Software via Dynamic Large-Block Encoding", in Proc. Proceedings of the 33rd Annual ACM Symposium on Applied Computing, SAC 2018, Pau, France, April 09-13, 2018, 2018, ACM, pp. 1891-1898.

@inproceedings { BHK18,
	author = { Bohlender, Dimitri and Hamm, Daniel and Kowalewski, Stefan },
	title = { Cycle-Bounded Model Checking of PLC Software via Dynamic
		Large-Block Encoding },
	booktitle = { Proceedings of the 33rd Annual ACM Symposium on Applied
		Computing, SAC 2018, Pau, France, April 09-13, 2018 },
	publisher = { ACM },
	publishedas = { Druck Online },
	isbn = { 978-1-4503-5191-1 },
	language = { eng },
	pages = { 1891--1898 },
	year = { 2018 },
	timestamp = { 2018.01.10 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2018 },
}

Obster, M. and Kowalewski, S., "A Live Static Code Analysis Architecture for PLC Software", in Proc. Proceedings of IEEE International Conference on Emerging Technology & Factory Automation, 2017, IEEE, pp. 263-266.

@inproceedings { OK17,
	author = { Obster, Mathias and Kowalewski, Stefan },
	title = { A Live Static Code Analysis Architecture for PLC Software },
	booktitle = { Proceedings of IEEE International Conference on Emerging
		Technology & Factory Automation },
	publisher = { IEEE },
	publishedas = { Online },
	isbn = { 978-1-5090-6505-9 },
	issn = { 1946-0759 },
	language = { eng },
	pages = { 263--266 },
	year = { 2017 },
	timestamp = { 2017.11.23 },
	i11key = { conference },
	i11projectkey = { Arcade },
	url = { https://publications.embedded.rwth-aachen.de/file/7a },
	for_reporting_period = { 2017 },
}

Ulewicz, S., Vogel-Heuser, B., Simon, H., Bohlender, D., Obster, M., and Kowalewski, S., "A Priori Test Coverage Estimation for Automated Production Systems", in Proc. 2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), 2017, IEEE, pp. 1-4.

@inproceedings { UVS+17,
	author = { Ulewicz, Sebastian and Vogel-Heuser, Birgit and Simon,
		Hendrik and Bohlender, Dimitri and Obster, Mathias and
		Kowalewski, Stefan },
	title = { A Priori Test Coverage Estimation for Automated Production
		Systems },
	booktitle = { 2017 22nd IEEE International Conference on Emerging
		Technologies and Factory Automation (ETFA) },
	publisher = { IEEE },
	publishedas = { Druck Online },
	isbn = { 978-1-5090-6505-9 },
	issn = { 1946-0759 },
	language = { eng },
	pages = { 1--4 },
	year = { 2017 },
	timestamp = { 2017.10.27 },
	i11key = { conference },
	i11projectkey = { Arcade },
	url = { http://ieeexplore.ieee.org/document/8247704/ },
	for_reporting_period = { 2017 },
}

Bohlender, D., Simon, H., Kowalewski, S., and Hauck-Stattelmann, S., "Symbolische Ausführung zum Testen von SPS-Programmen", in Proc. Automation 2016, 07.06.2016-08.06.2016, Baden-Baden, Germany, 2016, VDI Verlag GmbH, pp. 77-88.

@inproceedings { BSKH16,
	author = { Bohlender, Dimitri and Simon, Hendrik and Kowalewski, Stefan
		and Hauck-Stattelmann, Stefan },
	title = { Symbolische Ausf{\"u}hrung zum Testen von SPS-Programmen },
	booktitle = { Automation 2016, 07.06.2016-08.06.2016, Baden-Baden, Germany },
	publisher = { VDI Verlag GmbH },
	publishedas = { Druck },
	isbn = { 978-3-18-092284-0 },
	language = { ger },
	pages = { 77--88 },
	year = { 2016 },
	timestamp = { 2016.08.03 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2016 },
}

Bohlender, D., Simon, H., Friedrich, N., Kowalewski, S., and Hauck-Stattelmann, S., "Concolic Test Generation for PLC Programs using Coverage Metrics", in Proc. 13th International Workshop on Discrete Event Systems, WODES 2016, Xi'an, China, May 30 - June 1, 2016, 2016, IEEE, pp. 432-437.

@inproceedings { BSF+16,
	author = { Bohlender, Dimitri and Simon, Hendrik and Friedrich, Nico
		and Kowalewski, Stefan and Hauck-Stattelmann, Stefan },
	title = { Concolic Test Generation for PLC Programs using Coverage
		Metrics },
	booktitle = { 13th International Workshop on Discrete Event Systems, WODES
		2016, Xi'an, China, May 30 - June 1, 2016 },
	publisher = { IEEE },
	publishedas = { Druck },
	isbn = { 978-1-5090-4190-9 },
	language = { eng },
	pages = { 432--437 },
	year = { 2016 },
	timestamp = { 2016.06.27 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2016 },
}

Bohlender, D., Simon, H., and Kowalewski, S., "Symbolic Verification of PLC Safety-Applications based on PLCopen Automata", in Proc. 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, MBMV 2016, Freiburg im Breisgau, Germany, March 1-2, 2016., 2016, Albert-Ludwigs-Universität Freiburg, pp. 33-45.

@inproceedings { BSK16,
	author = { Bohlender, Dimitri and Simon, Hendrik and Kowalewski, Stefan },
	editor = { Ralf Wimmer },
	title = { Symbolic Verification of PLC Safety-Applications based on
		PLCopen Automata },
	booktitle = { 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen
		zur Modellierung und Verifikation von Schaltungen und
		Systemen, MBMV 2016, Freiburg im Breisgau, Germany, March
		1-2, 2016. },
	publisher = { Albert-Ludwigs-Universit{\"{a}}t Freiburg },
	publishedas = { Online },
	isbn = { 978-3-00-052380-9 },
	language = { eng },
	pages = { 33--45 },
	year = { 2016 },
	timestamp = { 2016.03.03 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2016 },
}

Biallas, S., Friedrich, N., Simon, H., and Kowalewski, S., "Automatic Error Cause Localization of Faulty PLC Programs", IFAC-PapersOnLine, vol. 48, pp. 79-84, 2015

@article { BFSK15,
	author = { Biallas, Sebastian and  Friedrich, Nico and Simon, Hendrik
		and Kowalewski, Stefan },
	title = { Automatic Error Cause Localization of Faulty PLC Programs },
	journal = { IFAC-PapersOnLine },
	year = { 2015 },
	volume = { 48 },
	pages = { 79--84 },
	publisher = { Elsevier Ltd },
	publishedas = { Online Druck },
	issn = { 1474-6670 },
	i11key = { conference },
	i11projectkey = { Arcade },
	language = { eng },
	url = { http://www.sciencedirect.com/science/article/pii/S2405896315007156 },
	timestamp = { 2015.09.21 },
	for_reporting_period = { 2015 },
}

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, 2015, VDI, pp. 100-111.

@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 },
	publisher = { VDI },
	publishedas = { Druck },
	language = { ger },
	pages = { 100--111 },
	year = { 2015 },
	timestamp = { 2015.07.08 },
	i11key = { conference },
	i11projectkey = { Arcade },
	url = { {http://publications.embedded.rwth-aachen.de/file/5r} },
	for_reporting_period = { 2015 },
}

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, 2015, vol. 9109 in Lecture Notes in Computer Science, Springer International Publishing, pp. 585-588.

@inproceedings { HBS+15,
	keywords = { Static Analysis; Abstract Interpretation; Programmable Logic
		Controllers },
	author = { Hauck-Stattelmann, Stefan and Biallas, Sebastian and
		Schlich, Bastian and Kowalewski, Stefan and Jetley, Raoul },
	editor = { Bj{\o}rner, Nikolaj and de Boer, Frank },
	title = { Analyzing the Restart Behavior of Industrial Control
		Applications },
	booktitle = { FM 2015: Formal Methods },
	series = { Lecture Notes in Computer Science },
	volume = { 9109 },
	publisher = { Springer International Publishing },
	publishedas = { Druck Online },
	isbn = { 978-3-319-19248-2 },
	language = { eng },
	pages = { 585--588 },
	year = { 2015 },
	timestamp = { 2015.06.03 },
	i11key = { conference },
	i11projectkey = { Arcade },
	url = { http://publications.embedded.rwth-aachen.de/file/5u },
	for_reporting_period = { 2015 },
}

Gückel, D., "Synthesis of State Space Generators for Model Checking Microcontroller Code," PhD Thesis , RWTH Aachen, 2014.

@phdthesis { Gue14,
	institution = { RWTH Aachen },
	keywords = { formal verification, model checking, hardware description,
		retargeting, embedded software },
	number = { AIB-2014-15 },
	timestamp = { 2015.06.01 },
	author = { G{\"u}ckel, Dominique },
	title = { {S}ynthesis of {S}tate {S}pace {G}enerators for {M}odel
		{C}hecking {M}icrocontroller {C}ode },
	school = { Fakult{\"a}t f{\"u}r Mathematik, Informatik und
		Naturwissenschaften der RWTH Aachen },
	type = { Dissertation },
	year = { 2014 },
	month = { November },
	i11key = { thesis },
	i11projectkey = { Arcade },
	url = { http://aib.informatik.rwth-aachen.de/2014/2014-15.pdf },
	for_reporting_period = { 2014 },
}

Stattelmann, S., Biallas, S., Schlich, B., and Kowalewski, S., "Applying Static Code Analysis on Industrial Controller Code", in Proc. 19th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), 2014, IEEE, Work in Progress Best Paper Award.

@inproceedings { SBSK14,
	author = { Stattelmann, Stefan and Biallas, Sebastian and Schlich,
		Bastian and Kowalewski, Stefan },
	title = { Applying Static Code Analysis on Industrial Controller Code },
	booktitle = { 19th IEEE International Conference on Emerging Technologies
		and Factory Automation (ETFA) },
	publisher = { IEEE },
	publishedas = { Druck Online },
	isbn = { 978-1-4799-4845-1 },
	language = { eng },
	year = { 2014 },
	timestamp = { 2014.09.17 },
	i11key = { conference },
	i11projectkey = { Arcade },
	note = { Work in Progress Best Paper Award },
	for_reporting_period = { 2014 },
}

Biallas, S., Kowalewski, S., Stattelmann, S., and Schlich, B., "Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code", in Proc. Proceedings of the 12th International Workshop on Discrete Event Systems, Cachan, France, 2014, IFAC, pp. 400-405.

@inproceedings { BKSS14,
	address = { Cachan, France },
	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 = { Proceedings of the 12th International Workshop on Discrete
		Event Systems },
	publisher = { IFAC },
	publishedas = { Druck Online },
	language = { eng },
	pages = { 400--405 },
	year = { 2014 },
	timestamp = { 2014.02.24 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2014 },
}

Brauer, J., "Automatic Abstraction for Bit-Vectors using Decision Procedures," PhD Thesis , 2013.

@phdthesis { Bra13,
	author = { Brauer, J{\"o}rg },
	title = { {A}utomatic {A}bstraction for {B}it-{V}ectors using
		{D}ecision {P}rocedures },
	school = { Fakult{\"a}t f{\"u}r Mathematik, Informatik und
		Naturwissenschaften der RWTH Aachen },
	type = { Dissertation },
	year = { 2013 },
	month = { November },
	issn = { 0935–3232 },
	i11key = { thesis },
	url = { http://publications.embedded.rwth-aachen.de/file/4y },
	keywords = { abstract interpretation, automatic abstraction, sat solving,
		decision procedures },
	i11projectkey = { Arcade },
	note = { AIB-2013-14 },
	timestamp = { 2014.02.03 },
	for_reporting_period = { 2013 },
}

Brauer, J., King, A., and Kowalewski, S., "Abstract interpretation of microcontroller code: Intervals meet congruences", Science of Computer Programming. Methods of Software Design: Techniques and Applications, vol. 78, issue 7, pp. 862-883, 2013

@article { BKK13,
	author = { Brauer, J{\"o}rg and King, Andy and Kowalewski, Stefan },
	title = { Abstract interpretation of microcontroller code: Intervals
		meet congruences },
	journal = { Science of Computer Programming. Methods of Software Design:
		Techniques and Applications },
	year = { 2013 },
	volume = { 78, issue 7 },
	pages = { 862--883 },
	publisher = { Elsevier },
	publishedas = { Druck },
	issn = { 0167-6423 },
	i11key = { journal },
	language = { eng },
	timestamp = { 2013.07.08 },
	i11projectkey = { Arcade },
	for_reporting_period = { 2013 },
}

Biallas, S., Giacobbe, M., and Kowalewski, S., "Predicate Abstraction for Programmable Logic Controllers", in Proc. 18th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2013), 2013, vol. 8187 in Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 123-138.

@inproceedings { BGK13,
	author = { Biallas, Sebastian and Giacobbe, Mirco and Kowalewski,
		Stefan },
	editor = { Pecheur, Charles and Dierkes, Michael },
	title = { Predicate Abstraction for Programmable Logic Controllers },
	booktitle = { 18th International Workshop on Formal Methods for Industrial
		Critical Systems (FMICS 2013) },
	series = { Lecture Notes in Computer Science },
	number = { 8187 },
	publisher = { Springer Berlin Heidelberg },
	publishedas = { Druck },
	isbn = { 978-3-642-41009-3 },
	language = { eng },
	pages = { 123--138 },
	year = { 2013 },
	timestamp = { 2013.06.27 },
	i11key = { conference },
	i11projectkey = { Arcade },
	volume = { 8187 },
	url = { http://publications.embedded.rwth-aachen.de/file/4u },
	for_reporting_period = { 2013 },
}

Biallas, S., Bohlender, D., and Kowalewski, S., "Boolean and Modular Abstractions for Programmable Logic Controllers", in Proc. Dependable Control of Discrete Systems (DCDS'13), 2013, IEEE, pp. 97-102.

@inproceedings { BBK13,
	author = { Biallas, Sebastian and Bohlender, Dimitri and Kowalewski,
		Stefan },
	title = { Boolean and Modular Abstractions for Programmable Logic
		Controllers },
	booktitle = { Dependable Control of Discrete Systems (DCDS'13) },
	publisher = { IEEE },
	publishedas = { Druck },
	isbn = { 978-3-902823-49-6 },
	issn = { 1474-6670 },
	language = { eng },
	pages = { 97--102 },
	year = { 2013 },
	timestamp = { 2013.06.06 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2013 },
}

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, 2013 in VDI Berichte, VDI-Verlag, pp. 75-79, Langfassung auf CD-ROM.

@inproceedings { BKK+13,
	author = { Biallas, Sebastian and Kamin, Volker and Kowalewski, Stefan
		and Schlich, Bastian and Sehestedt, Stephan and Stattelmann,
		Stefan },
	editor = { VDI Wissensforum },
	title = { Verifikation von sicherheitsgerichteten SPS-Programmen mit
		Hilfe von Safety-Automaten },
	booktitle = { Automation 2013 },
	series = { VDI Berichte },
	publisher = { VDI-Verlag },
	publishedas = { Druck },
	isbn = { 978-3-18-092209-6 },
	language = { ger },
	pages = { 75--79 },
	year = { 2013 },
	timestamp = { 2013.04.16 },
	i11key = { conference },
	i11projectkey = { Arcade },
	note = { Langfassung auf CD-ROM },
	for_reporting_period = { 2013 },
}

Biallas, S., Brauer, J., and Kowalewski, S., "Arcade.PLC: A Verification Platform for Programmable Logic Controllers", in Proc. Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering, 2012 in ASE 2012, ACM, pp. 338-341.

@inproceedings { BBK12b,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
		Stefan },
	title = { {Arcade.PLC}: A Verification Platform for Programmable Logic
		Controllers },
	booktitle = { Proceedings of the 27th IEEE/ACM International Conference on
		Automated Software Engineering },
	series = { ASE 2012 },
	publisher = { ACM },
	publishedas = { Druck Online },
	isbn = { 978-1-4503-1204-2 },
	language = { eng },
	pages = { 338--341 },
	year = { 2012 },
	timestamp = { 2012.09.16 },
	i11key = { conference },
	i11projectkey = { Arcade },
	url = { http://publications.embedded.rwth-aachen.de/file/3w },
	for_reporting_period = { 2012 },
}

Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse -- Formale Verifikation für SPS-Programme", Automatisierungstechnische Praxis (atp EDITION), 54. Jahrgang, 7-8/2012, pp. 68-75, 2012

@article { BKS12c,
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Automatische Wertebereichsanalyse -- Formale Verifikation
		f{\"u}r SPS-Programme },
	journal = { Automatisierungstechnische Praxis (atp EDITION), 54.
		Jahrgang, 7-8/2012 },
	year = { 2012 },
	pages = { 68--75 },
	publisher = { Oldenbourg Industrieverlag },
	publishedas = { Druck },
	issn = { 2190-4111 },
	i11key = { journal },
	i11projectkey = { Arcade },
	language = { ger },
	timestamp = { 2012.08.02 },
	for_reporting_period = { 2012 },
}

Biallas, S., Kowalewski, S., and Schlich, B., "Range and Value-Set Analysis for Programmable Logic Controllers", in Proc. Proceedings of the 11th International Workshop on Discrete Event Systems, Guadalajara, Mexico, 2012, IFAC, pp. 378-383.

@inproceedings { BKS12b,
	address = { Guadalajara, Mexico },
	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 },
	publishedas = { Druck Online },
	isbn = { 978-3-902823-28-1 },
	language = { eng },
	pages = { 378--383 },
	year = { 2012 },
	timestamp = { 2012.06.26 },
	i11key = { conference },
	i11projectkey = { Arcade },
	url = { http://publications.embedded.rwth-aachen.de/file/3x },
	for_reporting_period = { 2012 },
}

Biallas, S., Brauer, J., King, A., and Kowalewski, S., "Loop Leaping with Closures", in Proc. 19th Static Analysis Symposium, 2012 in Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 214-230.

@inproceedings { BBKK12,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and King, Andy and
		Kowalewski, Stefan },
	editor = { Min{\'e}, Antoine and Schmidt, David },
	title = { Loop Leaping with Closures },
	booktitle = { 19th Static Analysis Symposium },
	series = { Lecture Notes in Computer Science },
	publisher = { Springer Berlin Heidelberg },
	publishedas = { Druck Online },
	isbn = { 978-3-642-33124-4 },
	language = { eng },
	pages = { 214--230 },
	year = { 2012 },
	timestamp = { 2012.05.22 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2012 },
}

Biallas, S., Kowalewski, S., and Schlich, B., "Automatische Wertebereichsanalyse von SPS-Programmen", in Proc. AUTOMATION 2012, Baden-Baden, Germany, Düsseldorf, 2012 in VDI-Berichte, VDI-Verlag, pp. 79-83, Long version (12 pages) on CD-ROM.

@inproceedings { BKS12a,
	address = { D{\"u}sseldorf },
	author = { Biallas, Sebastian and Kowalewski, Stefan and Schlich,
		Bastian },
	title = { Automatische Wertebereichsanalyse von SPS-Programmen },
	booktitle = { AUTOMATION 2012, Baden-Baden, Germany },
	publisher = { VDI-Verlag },
	publishedas = { Druck },
	series = { VDI-Berichte },
	number = { 2171 },
	isbn = { 978-3-18-092171-6 },
	language = { ger },
	pages = { 79--83 },
	year = { 2012 },
	timestamp = { 2012.04.20 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2012 },
	note = { Long version (12 pages) on CD-ROM },
}

Brauer, J. and Simon, A., "Inferring Definite Counterexamples Through Under-Approximation", in Proc. NASA Formal Methods, 2012, vol. 7226 in Lecture Notes in Computer Science, Springer, pp. 54-69.

@inproceedings { BS12,
	author = { Brauer, J{\"o}rg and Simon, Axel },
	title = { Inferring Definite Counterexamples Through
		Under-Approximation },
	booktitle = { NASA Formal Methods },
	year = { 2012 },
	series = { Lecture Notes in Computer Science },
	publisher = { Springer },
	publishedas = { Druck },
	language = { eng },
	volume = { 7226 },
	isbn = { 978-3-642-28890-6 },
	pages = { 54--69 },
	timestamp = { 2012.01.24 },
	i11projectkey = { Arcade },
	i11key = { conference },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bs12.pdf },
	for_reporting_period = { 2012 },
}

Biallas, S., Kowalewski, S., and Schlich, B., "Leistungsfähige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse", in Proc. AUTOMATION 2011, Baden-Baden, Germany, Düsseldorf, 2011 in VDI-Berichte, VDI-Verlag, pp. 67-72.

@inproceedings { BKS11,
	address = { D{\"u}sseldorf },
	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 = { AUTOMATION 2011, Baden-Baden, Germany },
	isbn = { 978-3-18-092143-3 },
	issn = { 0083-5560 },
	number = { 2143 },
	pages = { 67--72 },
	publisher = { VDI-Verlag },
	publishedas = { Druck },
	series = { VDI-Berichte },
	language = { eng },
	year = { 2011 },
	timestamp = { 2011.04.20 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2011 },
}

Brauer, J., King, A., and Kriener, J., "Existential Quantification as Incremental SAT", in Proc. Computer Aided Verification (CAV 2011), 2011, vol. 6806 in Lecture Notes in Computer Science, Springer, pp. 191-207.

@inproceedings { BKK11a,
	author = { Brauer, J{\"o}rg and King, Andy and Kriener, Jael },
	title = { Existential Quantification as Incremental SAT },
	booktitle = { Computer Aided Verification (CAV 2011) },
	pages = { 191-207 },
	volume = { 6806 },
	series = { Lecture Notes in Computer Science },
	editor = { Gopalakrishnan, Ganesh and Qadeer, Shaz },
	publisher = { Springer },
	issn = { 0302-9743 },
	isbn = { 978-3-642-22110-1 },
	i11key = { conference },
	timestamp = { 2011.03.22 },
	year = { 2011 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bkk11a.pdf },
	language = { eng },
	publishedas = { Druck Online },
	i11projectkey = { Arcade },
	for_reporting_period = { 2011 },
}

Biallas, S., Brauer, J., and Kowalewski, S., "SAT-Based Abstraction Refinement for Programmable Logic Controllers", in Proc. Dependable Control of Discrete Systems (DCDS'11), 2011, IEEE, pp. 96-101.

@inproceedings { BBK11,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and Kowalewski,
		Stefan },
	title = { SAT-Based Abstraction Refinement for Programmable Logic
		Controllers },
	booktitle = { Dependable Control of Discrete Systems (DCDS'11) },
	language = { eng },
	publisher = { IEEE },
	publishedas = { Druck },
	isbn = { 978-1-4244-8969-5 },
	pages = { 96--101 },
	i11key = { conference },
	i11projectkey = { Arcade },
	year = { 2011 },
	timestamp = { 2011.03.15 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbk11.pdf },
	for_reporting_period = { 2011 },
}

Brauer, J. and King, A., "Approximate Quantifier Elimination for Propositional Boolean Formulae", in Proc. NASA Formal Methods Symposium (NFM 2011), 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 },
	isbn = { 978-3-642-20397-8 },
	pages = { 73--88 },
	volume = { 6617 },
	year = { 2011 },
	timestamp = { 2011.03.04 },
	publishedas = { Druck Online },
	language = { eng },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bk11b.pdf },
	i11projectkey = { Arcade },
	for_reporting_period = { 2011 },
}

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 },
	issn = { 0167-6423 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:sbk10.pdf },
	i11key = { journal },
	timestamp = { 2010.12.06 },
	i11projectkey = { Arcade },
	for_reporting_period = { 2011 },
}

Biallas, S., Brauer, J., Gückel, D., and Kowalewski, S., "On-The-Fly Path Reduction", Electronic Notes in Theoretical Computer Science, vol. 274C, pp. 3-16, 2011, 4th International Workshop on Harnessing Theories for Tool Support in Software (TTSS 2010)

@article { BBGK10,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and G{\"u}ckel,
		Dominique and Kowalewski, Stefan },
	title = { On-The-Fly Path Reduction },
	journal = { Electronic Notes in Theoretical Computer Science },
	year = { 2011 },
	volume = { 274C },
	pages = { 3--16 },
	publisher = { Elsevier },
	note = { 4th International Workshop on Harnessing Theories for Tool
		Support in Software (TTSS 2010) },
	issn = { 1571-0661 },
	i11key = { conference },
	i11projectkey = { Arcade },
	publishedas = { Online },
	language = { eng },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbgk10.pdf },
	timestamp = { 2010.10.05 },
	for_reporting_period = { 2010 },
}

Biallas, S., Brauer, J., Kowalewski, S., and Schlich, B., "Automatically Deriving Symbolic Invariants for PLC Programs Written in IL", in Proc. FORMS/FORMAT 2010, 2011, Springer Berlin Heidelberg, pp. 237-245.

@inproceedings { BBKS10,
	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 = { FORMS/FORMAT 2010 },
	editor = { Schnieder, Eckehard and Tarnai, Geza },
	publisher = { Springer Berlin Heidelberg },
	publishedas = { Druck },
	language = { eng },
	year = { 2011 },
	timestamp = { 2010.08.19 },
	isbn = { 978-3-642-14261-1 },
	pages = { 237--245 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbks10.pdf },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2010 },
}

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, Berkeley, CA, USA, 2010, USENIX Association, pp. 2-12.

@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 },
	location = { Vancouver, BC, Canada },
	pages = { 2--12 },
	numpages = { 1 },
	publisher = { USENIX Association },
	address = { Berkeley, CA, USA },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbk10.pdf },
	timestamp = { 2010.07.19 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2010 },
}

Brauer, J., Kamin, V., Kowalewski, S., and Noll, T., "Loop Refinement using Octagons and Satisfiability", in Proc. Proceedings of the 5th international conference on Systems software verification, Berkeley, CA, USA, 2010, USENIX Association, pp. 1-9.

@inproceedings { BKKN10,
	author = { Brauer, J{\"o}rg and Kamin, Volker and Kowalewski, Stefan
		and Noll, Thomas },
	title = { Loop Refinement using Octagons and Satisfiability },
	booktitle = { Proceedings of the 5th international conference on Systems
		software verification },
	year = { 2010 },
	location = { Vancouver, BC, Canada },
	pages = { 1--9 },
	timestamp = { 2010.07.19 },
	publisher = { USENIX Association },
	address = { Berkeley, CA, USA },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bkkn10.pdf },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2010 },
}

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.

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

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, IEEE, pp. 118-127.

@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 },
	pages = { 118--127 },
	publisher = { IEEE },
	timestamp = { 2010.06.01 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:gbk10.pdf },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2010 },
}

Brauer, J. and King, A., "Automatic Abstraction for Intervals using Boolean Formulae", in Proc. Static Analysis Symposium (SAS 2010), Perpignan, France, 2010, vol. 6337 in Lecture Notes in Computer Science, Springer, pp. 167-183.

@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 },
	volume = { 6337 },
	pages = { 167--183 },
	timestamp = { 2010.05.04 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bk10.pdf },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2010 },
}

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.

@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 },
	publisher = { ACM },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:BNS10.pdf },
	timestamp = { 2010.04.01 },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2010 },
}

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, IEEE, pp. 313-316.

@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 },
	publisher = { IEEE },
	pages = { 313--316 },
	owner = { gueckel },
	i11key = { conference },
	url = { http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5491761 },
	timestamp = { 2010.03.08 },
	i11projectkey = { Arcade },
	for_reporting_period = { 2010 },
}

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, ifak Magdeburg, pp. 49-57.

@inproceedings { BFK+10,
	author = { Biallas, Sebastian and Frey, Georg and Kowalewski, Stefan
		and Schlich, Bastian and Soliman, Doaa },
	title = { Formale Verifikation von Sicherheits-Funktionsbausteinen der
		PLCopen auf Modell- und Code-Ebene },
	booktitle = { Tagungsband Entwicklung und Betrieb komplexer
		Automatisierungssysteme (EKA 2010) },
	publisher = { ifak Magdeburg },
	publishedas = { Druck },
	language = { ger },
	pages = { 49--57 },
	year = { 2010 },
	isbn = { 978-3-940961-41-9 },
	location = { Magdeburg, Germany },
	i11key = { conference },
	i11projectkey = { Arcade },
	for_reporting_period = { 2010 },
}

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 },
	i11projectkey = { Arcade },
	for_reporting_period = { Old },
}