Publications

[BFSK15] PDF   BIB
Biallas, S., Friedrich, N., Simon, H., and Kowalewski, S., "Automatic Error Cause Localization of Faulty PLC Programs", in Proc. Dependable Control of Discrete Systems (DCDS'15), 2015, To appear.

Automatic Error Cause Localization of Faulty PLC Programs

Bibtex entry :

@conference {   BFSK15,
	author = { Biallas, Sebastian and  Friedrich, Nico and Simon, Hendrik
		and Kowalewski, Stefan },
	title = { Automatic Error Cause Localization of Faulty PLC Programs },
	booktitle = { Dependable Control of Discrete Systems (DCDS'15) },
	year = { 2015 },
	timestamp = { 2015.12.05 },
	language = { eng },
	i11key = { conference },
	i11projectkey = { Arcade },
	note = { To appear },
	for_reporting_period = { 2015 },
}
[BSK+15] PDF   BIB
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, To appear.

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

Bibtex entry :

@conference {   BSK+15,
	author = { Biallas, Sebastian and Simon, Hendrik and Kowalewski, Stefan
		and Hauck-Stattelmann, Stefan and Schlich, Bastian },
	title = { Automatische Testfallgenerierung für SPS-Programme mittels
		Zeilenüberdeckung },
	booktitle = { AUTOMATION 2015 },
	year = { 2015 },
	timestamp = { 2015.12.05 },
	language = { deu },
	i11key = { conference },
	i11projectkey = { Arcade },
	note = { To appear },
	for_reporting_period = { 2015 },
}
[SBSK14] PDF   BIB
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.

Applying Static Code Analysis on Industrial Controller Code

Bibtex entry :

@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 },
	for_reporting_period = { 2014 },
}
[BKSS14] PDF   BIB
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.

Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code

Bibtex entry :

@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 },
}
[BKSS14] PDF   BIB
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.

Efficient Handling of States in Abstract Interpretation of Industrial Programmable Logic Controller Code

Bibtex entry :

@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 },
}
[Bra13] PDF   BIB
Brauer, J., "Automatic Abstraction for Bit-Vectors using Decision Procedures," PhD Thesis , 2013.

{A}utomatic {A}bstraction for {B}it-{V}ectors using {D}ecision {P}rocedures

Bibtex entry :

@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 },
}
[BKK13] PDF   BIB
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

Abstract interpretation of microcontroller code: Intervals meet congruences

Bibtex entry :

@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 },
}
[BGK13] PDF   BIB
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.

Predicate Abstraction for Programmable Logic Controllers

Bibtex entry :

@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 },
}
[BBK13] PDF   BIB
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.

Boolean and Modular Abstractions for Programmable Logic Controllers

Bibtex entry :

@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 },
}
[BKK+13] PDF   BIB
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.

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

Bibtex entry :

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

{Arcade.PLC}: A Verification Platform for Programmable Logic Controllers

Bibtex entry :

@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 },
}
[BKK12] PDF   BIB
Brauer, J., King, A., and Kowalewski, S., "Abstract Interpretation of Microcontroller Code: Intervals meet Congruences", Science of Computer Programming, vol. 77, 2012, To appear

Abstract {I}nterpretation of {M}icrocontroller {C}ode: {I}ntervals meet {C}ongruences

Bibtex entry :

@article { BKK12,
	month = { July },
	doi = { 10.1016/j.scico.2012.06.001 },
	author = { Brauer, J{\"o}rg and King, Andy and Kowalewski, Stefan },
	title = { Abstract {I}nterpretation of {M}icrocontroller {C}ode:
		{I}ntervals meet {C}ongruences },
	journal = { Science of Computer Programming },
	year = { 2012 },
	volume = { 77 },
	publisher = { Elsevier },
	publishedas = { Online Druck },
	issn = { 0167-6423 },
	i11key = { journal },
	language = { eng },
	url = { http://www.sciencedirect.com/science/article/pii/S0167642312001116" },
	note = { To appear },
	i11projectkey = { Arcade },
	timestamp = { 2012.09.06 },
	for_reporting_period = { 2012 },
}
[BKS12c] PDF   BIB
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-74, 2012

Automatische Wertebereichsanalyse -- Formale Verifikation f{\"u}r SPS-Programme

Bibtex entry :

@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--74 },
	publisher = { Oldenbourg Industrieverlag },
	publishedas = { Druck },
	issn = { 2190-4111 },
	i11key = { journal },
	language = { ger },
	i11projectkey = { Arcade },
	timestamp = { 2012.08.02 },
	for_reporting_period = { 2012 },
}
[BKS12b] PDF   BIB
Biallas, S., Kowalewski, S., and Schlich, B., "Range and Value-Set Analysis for Programmable Logic Controllers", in Proc. Proceedings of the 11th International Workshop on Discrete Event Systems, Guadalajara, Mexico, 2012, IFAC, pp. 378-383.

Range and Value-Set Analysis for Programmable Logic Controllers

Bibtex entry :

@inproceedings { BKS12b,
	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 },
}
[BBKK12] PDF   BIB
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.

Loop Leaping with Closures

Bibtex entry :

@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 },
}
[BKS12a] PDF   BIB
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.

Automatische Wertebereichsanalyse von SPS-Programmen

Bibtex entry :

@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 },
}
[BS12] PDF   BIB
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.

Inferring Definite Counterexamples Through Under-Approximation

Bibtex entry :

@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 },
}
[BKS11] PDF   BIB
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.

Leistungsf{\"a}hige Verifikation von industriellen SPS-Programmen mittels Model-Checking und statischer Analyse

Bibtex entry :

@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 },
}
[BKK11a] PDF   Slides   BIB
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.

Existential Quantification as Incremental SAT

Bibtex entry :

@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 },
}
[BBK11] PDF   BIB
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.

SAT-Based Abstraction Refinement for Programmable Logic Controllers

Bibtex entry :

@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 },
}
[BK11b] PDF   Slides   BIB
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.

Approximate Quantifier Elimination for Propositional Boolean Formulae

Bibtex entry :

@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 },
}
[SBK11] PDF   BIB
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

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

Bibtex entry :

@article { SBK11,
	author = { Schlich, Bastian and Brauer, J{\"o}rg and Kowalewski, Stefan },
	title = { Application of Static Analyses for State Space Reduction to
		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 },
}
[BBGK10] PDF   BIB
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)

On-The-Fly Path Reduction

Bibtex entry :

@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 },
}
[BBKS10] PDF   BIB
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.

Automatically Deriving Symbolic Invariants for {PLC} Programs Written in {IL}

Bibtex entry :

@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 },
}
[BBK10] PDF   BIB
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.

Counterexample-guided abstraction refinement for {PLCs}

Bibtex entry :

@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 },
}
[BKKN10] PDF   BIB
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.

Loop Refinement using Octagons and Satisfiability

Bibtex entry :

@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 },
}
[BKK10] PDF   Slides   BIB
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.

Range Analysis of Microcontroller Code using Bit-Level Congruences

Bibtex entry :

@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 },
}
[GBK10] PDF   BIB
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.

A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification

Bibtex entry :

@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 },
}
[BK10] PDF   Slides   BIB
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.

Automatic Abstraction for Intervals using Boolean Formulae

Bibtex entry :

@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 },
}
[BNS10] PDF   BIB
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.

Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software

Bibtex entry :

@inproceedings { BNS10,
	author = { Brauer, J{\"o}rg and Noll, Thomas and Schlich, Bastian },
	title = { Interval Analysis of Microcontroller Code using Abstract
		Interpretation of Hardware and Software },
	booktitle = { 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 },
}
[GSBK10] PDF   BIB
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.

Synthesizing Simulators for Model Checking Microcontroller Binary Code

Bibtex entry :

@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 },
}
[BFK+10] PDF   BIB
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.

Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene

Bibtex entry :

@inproceedings { BFK+10,
	author = { Biallas, Sebastian and Frey, Georg and Kowalewski, Stefan
		and Schlich, Bastian and Soliman, Doaa },
	title = { Formale Verifikation von Sicherheits-Funktionsbausteinen der
		PLCopen auf Modell- und Code-Ebene },
	booktitle = { 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 },
}
[BSK09b] PDF   BIB
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)

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