Lehrstuhl Informatik 11
Professor Dr.-Ing. Stefan Kowalewski

Lehrstuhl

Neuigkeiten
Mitarbeiter
Kontakt
Stellen
Pressespiegel
Impressum

Forschung

Projekte
Publikationen

Lehre

Automatisierungstechnik
Klausuranmeldefristen
Sommersemester 13
Wintersemester 12/13
Sommersemester 12
Vorherige Semester
Abschlussarbeiten
Vortrags- & Kolloquiumstermine

Events

SE'13 (Aachen)
Vorherige Events

PDF ExportSie befinden sich hier: Lehrstuhl » Mitarbeiter » Dipl.-Inf. Jörg Brauer

Dipl.-Inf. Jörg Brauer

Kontakt

Wissenschaftlicher Mitarbeiter

Tel. +49 241 80 21156
Fax +49 241 80 22150

Email: brauer[at]embedded[dot]rwth-aachen[dot]de

Adresse: Ahornstr. 55, 52074 Aachen, Germany
Büro: Raum 2325 (Gebäude H)

Sprechstunde: nach Vereinbarung



Über mich

Ich bin derzeit Doktorand am I11, wo ich das Projekt [mc]square leite. Bei [mc]square handelt es sich um einem Model-Checker für Binärcode auf verschiedenen Mikrocontroller-Plattformen. Hierbei konzentriere ich mich vor allem auf die Entwicklung von statischen Analysen zur Fehlererkennung sowie zur Abstraktion. Bevor ich zum Lehrstuhl Informatik 11 an die RWTH Aachen gewechselt bin, habe ich Informatik an der Christian-Albrechts-Universität zu Kiel studiert und war am NICTA, wo ich an Goanna, einem Tool zur statischen Analyse von C/C++ Code gearbeitet habe.

Mein Lebenslauf ist hier erhältlich.

Neuigkeiten

Aktivitäten

Forschungsschwerpunkte

  • Statische Analyse von Mikrocontroller Software
  • Abstrakte Interpretation
  • Pointer Analyse
  • Formale Verifikation
  • Software Model-Checking

Zusammenfassend beschäftige ich mich mit der Fragestellung, wie man Prinzipien der theoretischen Informatik anwenden kann, um Low-Level Programme zu verifizieren. Hierbei interessiert mich insbesondere die Anwendung von SAT und SMT Solvern und deren Zusammenspiel mit abstrakter Interpretation. Bei Interesse an diesem Thema empfehle ich, einen Blick auf mein SAS'10 Papier oder mein ESOP'11 Papier zu werfen, welche einen guten Überblick darüber geben, welche Präzision sich mit SAT-basierter abstrakter Interpretation erreichen läßt.

Abschlussarbeiten

Wir haben stets eine größere Anzahl von offenen Themen für Abschlussarbeiten, auch über die auf dieser Seite gelisteten Themen hinaus. Wenn Interesse daran besteht, die eigene Abschlussarbeit im Bereich der Software-Verifikation für eingebettete Systeme zu schreiben, dann kontaktiert mich bitte per E-Mail.

  • Offen
  • Laufend
    • Na Bai (Diplom): Datenflussanalyse für Speicherprogrammierbare Steuerungen
    • Mustafa Karafil (Diplom): Analyse von indirektem Kontrollfluss
  • Abgeschlossen
    • Sebastian Biallas (Diplom): Gegenbeispiel-geleitete Abstraktionsverfeinerung für speicherprogrammierbare Steuerungen
    • Frank Birbacher (Diplom): Relationale Analyse von SPSen mittels Kongruenzen
    • Lucas Brutschy (B.Sc.): Statische Analyse von Mikrocontrollerprogrammen mittels SAT- und SMT-Solving
    • Jörg Toborg (Diplom): Statische Analyse für den Renesas R8C/23 Tiny

Publikationen

Eine detaillierte Übersicht über meine Veröffentlichungen findet sich hier.

Journals

Publikations-Export
[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 },
	timestamp = { 2012.09.06 },
	for_reporting_period = { 2012 },
}
[BBK12a] PDF   BIB
Beckschulze, E., Brauer, J., and Kowalewski, S., "Access-Based Localization for Octagons", Electronic Notes in Theoretical Computer Science, pp. 29-40, 2012, Proceedings of the Fourth International Workshop on Numerical and Symbolic Abstract Domains, NSAD 2012

Access-Based Localization for Octagons

Bibtex entry :

@article { BBK12a,
	booktitle = { The Fourth International Workshop on Numerical and Symbolic
		Abstract Domains (NSAD 2012) },
	author = { Beckschulze, Eva and Brauer, J{\"o}rg and Kowalewski, Stefan },
	title = { Access-Based Localization for Octagons },
	journal = { Electronic Notes in Theoretical Computer Science },
	year = { 2012 },
	pages = { 29--40 },
	publisher = { Elsevier },
	publishedas = { Online },
	issn = { 1571-0661 },
	i11key = { journal },
	language = { eng },
	url = { http://www.sciencedirect.com/science/article/pii/S1571066112000564 },
	note = { Proceedings of the Fourth International Workshop on
		Numerical and Symbolic Abstract Domains, NSAD 2012 },
	timestamp = { 2012.07.17 },
	for_reporting_period = { 2012 },
}
[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 },
	for_reporting_period = { 2011 },
}
[RHS+10] PDF   BIB
Reinbacher, T., Horauer, M., Schlich, B., Brauer, J., and Scheuer, F., "Model Checking Embedded Software of an Industrial Knitting Machine", International Journal of Information Technology, Communications and Convergenceonvergence, pp. 186-205, 2010

Model Checking Embedded Software of an Industrial Knitting Machine

Bibtex entry :

@article { RHS+10,
	author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian
		and Brauer, J{\"o}rg and Scheuer, Florian },
	title = { Model Checking Embedded Software of an Industrial Knitting
		Machine },
	journal = { International Journal of Information Technology,
		Communications and Convergenceonvergence },
	year = { 2010 },
	pages = { 186--205 },
	publisher = { Inderscience Enterprises Ltd },
	publishedas = { Online Druck },
	issn = { 2042-3217 },
	i11key = { journal },
	language = { eng },
	url = { http://inderscience.metapress.com/content/y664g84625r780l0/fulltext.pdf },
	timestamp = { 2010.08.15 },
	for_reporting_period = { 2010 },
}

Begutachtete Konferenzen und Workshops

Publikations-Export
[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 },
	url = { http://publications.embedded.rwth-aachen.de/file/3w },
	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, To appear.

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 },
	note = { To appear },
	for_reporting_period = { 2012 },
}
[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 },
	i11key = { conference },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bs12.pdf },
	for_reporting_period = { 2012 },
}
[RBS+11] PDF   Slides   BIB
Reinbacher, T., Brauer, J., Schachinger, D., Steininger, A., and Kowalewski, S., "Automated Test-Trace Inspection for Microcontroller Binary Code", in Proc. RV, 2011, Springer, pp. 239-244.

Automated Test-Trace Inspection for Microcontroller Binary Code

Bibtex entry :

@inproceedings { RBS+11,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Schachinger,
		Daniel and Steininger, Andreas and Kowalewski, Stefan },
	title = { Automated Test-Trace Inspection for Microcontroller Binary
		Code },
	booktitle = { RV },
	publisher = { Springer },
	publishedas = { Druck },
	isbn = { 978-3-642-29859-2 },
	language = { eng },
	pages = { 239--244 },
	year = { 2011 },
	timestamp = { 2011.12.14 },
	i11key = { conference },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:rbs11.pdf },
	for_reporting_period = { 2011 },
}
[RB11] PDF   Slides   BIB
Reinbacher, T. and Brauer, J., "Precise Control Flow Reconstruction Using Boolean Logic", in Proc. International Conference on Embedded Software (EMSOFT 2011), 2011, ACM, pp. 117-126.

Precise Control Flow Reconstruction Using Boolean Logic

Bibtex entry :

@inproceedings { RB11,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg },
	editor = { Chakraborty, Samarjit and Jerraya, Ahmed and Baruah, Sanjoy
		K. and Fischmeister, Sebastian },
	title = { Precise Control Flow Reconstruction Using Boolean Logic },
	booktitle = { International Conference on Embedded Software (EMSOFT 2011) },
	publisher = { ACM },
	publishedas = { Druck Online },
	isbn = { 978-1-4503-0714-7 },
	language = { eng },
	pages = { 117--126 },
	year = { 2011 },
	timestamp = { 2011.07.03 },
	i11key = { conference },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:rb11.pdf },
	for_reporting_period = { 2011 },
}
[BHK+12] PDF   BIB
Brauer, J., Hansen, R. R., Kowalewski, S., Larsen, K. G., and Olesen, M. C., "Adaptable Value-Set Analysis for Low-Level Code", in Proc. 6th International Workshop on Systems Software Verification (SSV 2011), 2012, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 32-43.

Adaptable Value-Set Analysis for Low-Level Code

Bibtex entry :

@inproceedings { BHK+12,
	author = { Brauer, J{\"o}rg and Hansen, Rene Rydhof and Kowalewski,
		Stefan and Larsen, Kim G. and Olesen, Mads Chr. },
	title = { Adaptable Value-Set Analysis for Low-Level Code },
	booktitle = { 6th International Workshop on Systems Software Verification
		(SSV 2011) },
	publisher = { Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik },
	publishedas = { Druck Online },
	isbn = { 978-3-939897-36-1 },
	issn = { 2190-6807 },
	language = { eng },
	pages = { 32--43 },
	year = { 2012 },
	timestamp = { 2011.07.01 },
	i11key = { conference },
	url = { http://dx.doi.org/10.4230/OASIcs.SSV.2011.32 },
	for_reporting_period = { 2011 },
}
[RBH+11] PDF   Slides   BIB
Reinbacher, T., Brauer, J., Horauer, M., Steininger, A., and Kowalewski, S., "Past Time LTL Runtime Verification for Microcontroller Binary Code", in Proc. 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2011), 2011, vol. 6959 in Lecture Notes in Computer Science, Springer, pp. 37-51.

Past Time LTL Runtime Verification for Microcontroller Binary Code

Bibtex entry :

@inproceedings { RBH+11,
	volume = { 6959 },
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Steininger, Andreas and Kowalewski, Stefan },
	editor = { Sala{\"u}n, Gwen and Sch{\"a}tz, Bernhard },
	title = { Past Time LTL Runtime Verification for Microcontroller
		Binary Code },
	booktitle = { 16th International Workshop on Formal Methods for Industrial
		Critical Systems (FMICS 2011) },
	series = { Lecture Notes in Computer Science },
	publisher = { Springer },
	publishedas = { Druck Online },
	isbn = { 978-3-642-24430-8 },
	language = { eng },
	pages = { 37--51 },
	year = { 2011 },
	timestamp = { 2011.05.09 },
	i11key = { conference },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:rbh11.pdf },
	for_reporting_period = { 2011 },
}
[RSM+11] PDF   Slides   BIB
Reinbacher, T., Steininger, A., Müller, T., Horauer, M., Brauer, J., and Kowalewski, S., "Hardware Support for Efficient Testing of Embedded Software", in Proc. 7th ASME/IEEE Conference on Mechatronics and Embedded Systems and Applications (MESA 2011), 2011, ASME, pp. 3-12.

Hardware Support for Efficient Testing of Embedded Software

Bibtex entry :

@inproceedings { RSM+11,
	author = { Reinbacher, Thomas and Steininger, Andreas and M{\"u}ller,
		Tobias and Horauer, Martin and Brauer, J{\"o}rg and
		Kowalewski, Stefan },
	title = { Hardware Support for Efficient Testing of Embedded Software },
	booktitle = { 7th ASME/IEEE Conference on Mechatronics and Embedded
		Systems and Applications (MESA 2011) },
	publisher = { ASME },
	publishedas = { Druck Online },
	isbn = { 978-0-7918-5480-8 },
	language = { eng },
	pages = { 3--12 },
	year = { 2011 },
	timestamp = { 2011.04.29 },
	i11key = { conference },
	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 },
	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 },
	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 },
	for_reporting_period = { 2011 },
}
[BBSK11] PDF   BIB
Beckschulze, E., Brauer, J., Stollenwerk, A., and Kowalewski, S., "Analyzing Embedded Systems Code for Mixed-Critical Systems using Hybrid Memory Representations", in Proc. 2011 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops ISORCW 2011, 2011, IEEE, pp. 33-40.

Analyzing Embedded Systems Code for Mixed-Critical Systems using Hybrid Memory Representations

Bibtex entry :

@inproceedings { BBSK11,
	location = { Newport Beach, CA, USA },
	doi = { 10.1109/ISORCW.2011.40 },
	author = { Beckschulze, Eva and Brauer, J{\"o}rg and Stollenwerk,
		Andr{\'e} and Kowalewski, Stefan },
	title = { Analyzing Embedded Systems Code for Mixed-Critical Systems
		using Hybrid Memory Representations },
	booktitle = { 2011 14th IEEE International Symposium on
		Object/Component/Service-Oriented Real-Time Distributed
		Computing Workshops ISORCW 2011 },
	publisher = { IEEE },
	publishedas = { Druck Online },
	isbn = { 978-1-4577-0303-4 },
	language = { eng },
	pages = { 33--40 },
	year = { 2011 },
	timestamp = { 2010.12.23 },
	i11key = { conference },
	url = { http://publications.embedded.rwth-aachen.de/file/4f },
	for_reporting_period = { 2011 },
}
[BK11a] PDF   Slides   BIB
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.

Transfer Function Synthesis without Quantifier Elimination

Bibtex entry :

@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 },
	isbn = { 978-3-642-19717-8 },
	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 },
	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 },
	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 },
}
[RBH+10] PDF   BIB
Reinbacher, T., Brauer, J., Horauer, M., Steininger, A., and Kowalewski, S., "Test-Case Generation for Embedded Binary Code Using Abstract Interpretation", in Proc. Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2010), Selected Papers, Mikulov, Czech Republic, 2010, vol. 16 in OASICS, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, pp. 101-108, Best Paper Award.

Test-Case Generation for Embedded Binary Code Using Abstract Interpretation

Bibtex entry :

@inproceedings { RBH+10,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Steininger, Andreas and Kowalewski, Stefan },
	title = { Test-Case Generation for Embedded Binary Code Using Abstract
		Interpretation },
	booktitle = { Sixth Doctoral Workshop on Mathematical and Engineering
		Methods in Computer Science (MEMICS 2010), Selected Papers,
		Mikulov, Czech Republic },
	year = { 2010 },
	timestamp = { 2010.09.22 },
	publisher = { Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany },
	isbn = { 978-3-939897-22-4 },
	series = { OASICS },
	volume = { 16 },
	pages = { 101--108 },
	note = { Best Paper Award },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:rbh+10.pdf },
	i11key = { conference },
	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 },
	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 },
	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 },
	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 },
	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 },
	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 },
	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 },
	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 },
	for_reporting_period = { 2010 },
}
[BHS09] PDF   BIB
Brauer, J., Huuck, R., and Schlich, B., "Interprocedural Pointer Analysis in Goanna", Electronic Notes in Theoretical Computer Science, vol. 254, p. 65, 2009, Proceedings of the 4th International Workshop on Systems Software Verification (SSV 2009)

Interprocedural Pointer Analysis in Goanna

Bibtex entry :

@article { BHS09,
	author = { Brauer, J{\"o}rg and Huuck, Ralf and Schlich, Bastian },
	title = { Interprocedural Pointer Analysis in Goanna },
	journal = { Electronic Notes in Theoretical Computer Science },
	volume = { 254 },
	pages = { 65–83 },
	year = { 2009 },
	note = { Proceedings of the 4th International Workshop on Systems
		Software Verification (SSV 2009) },
	publisher = { Elsevier },
	issn = { 1571-0661 },
	url = { http://portal.acm.org/citation.cfm?id=1630458 },
	i11key = { conference },
	for_reporting_period = { Old },
}
[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 },
	for_reporting_period = { Old },
}
[BSRK09] PDF   BIB
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.

Stack Bounds Analysis of Microcontroller Assembly Code

Bibtex entry :

@inproceedings { BSRK09,
	author = { Brauer, J{\"o}rg and Schlich, Bastian and Reinbacher, Thomas
		and Kowalewski, Stefan },
	title = { Stack Bounds Analysis of Microcontroller Assembly Code },
	booktitle = { Workshop on Embedded Security (WESS 2009), Grenoble, France },
	year = { 2009 },
	publisher = { ACM Press },
	url = { http://portal.acm.org/citation.cfm?id=1631716.1631721 },
	i11key = { conference },
	for_reporting_period = { Old },
}
[RBHS09] PDF   BIB
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.

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

Bibtex entry :

@inproceedings { RBHS09,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Schlich, Bastian },
	booktitle = { Industrial Embedded Systems (SIES'09), Lausanne, Switzerland },
	doi = { 10.1109/SIES.2009.5196212 },
	isbn = { 978-1-4244-4109-9 },
	pages = { 161--170 },
	publisher = { IEEE Computer Society Press },
	title = { Refining Assembly Code Static Analysis for the Intel MCS-51
		Microcontroller },
	year = { 2009 },
	url = { http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5196212 },
	i11key = { conference },
	for_reporting_period = { Old },
}
[RHS+09] PDF   BIB
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, pp. 1-8.

Model Checking Assembly Code of an Industrial Knitting Machine

Bibtex entry :

@inproceedings { RHS+09,
	author = { Reinbacher, Thomas and Horauer, Martin and Schlich, Bastian
		and Brauer, J{\"o}rg and Scheuer, Florian },
	title = { Model Checking Assembly Code of an Industrial Knitting
		Machine },
	booktitle = { Embedded and Multimedia Computing (EM-Com 2009), Jeju, Korea },
	year = { 2009 },
	publisher = { IEEE Computer Society Press },
	pages = { 1--8 },
	i11key = { conference },
	url = { http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5402986 },
	for_reporting_period = { 2010 },
}
[SBWK09] PDF   BIB
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, pp. 28-33.

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

Bibtex entry :

@inproceedings { SBWK09,
	author = { Schlich, Bastian and Brauer, J{\"o}rg and Wernerus, J{\"o}rg
		and  Kowalewski, Stefan },
	booktitle = { Dependable Control of Discrete Systems (DCDS'09), Bari,
		Italy },
	isbn = { 978-3-902661-44-9 },
	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 },
	pages = { 28--33 },
	for_reporting_period = { Old },
}
[SNBB09] PDF   BIB
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, vol. 6405 in Lecture Notes in Computer Science, Springer, pp. 5-20.

Reduction of Interrupt Handler Executions for Model Checking Embedded Software

Bibtex entry :

@inproceedings { SNBB09,
	author = { Schlich, B. and Noll, T. and Brauer, J. and Brutschy, L. },
	title = { Reduction of Interrupt Handler Executions for Model Checking
		Embedded Software },
	booktitle = { Haifa Verification Conference (HVC 2009), Haifa, Israel },
	year = { 2009 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:SNBB09.pdf },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	volume = { 6405 },
	pages = { 5--20 },
	i11key = { conference },
	for_reporting_period = { Old },
}
[HFSB08] PDF   BIB
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.

Goanna: Syntactic Software Model Checking

Bibtex entry :

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

Lehre


RWTH Aachen - Lehrstuhl Informatik 11 - Ahornstr. 55 - 52074 Aachen - Deutschland