I moved to Bremen.

Prior to moving up north, I used to be a PhD student heading the [mc]square project. [mc]square is a verification platform for microcontroller binary code. The key idea in [mc]square is to combine different formal methods in order to analyze hardware-specific microcontroller code. My own focus is the development of static analysis and abtract interpretation techniques specifically suited for verifying bit-twiddling programs. I am also involved in the CEVTES project, which is a joint project with the TU Vienna and the UAS Technikum Vienna on test-case generation for binary code.

Before I joined the Embedded Software Laboratory, I received my diploma degree from the Christian-Albrechts University of Kiel and visited NICTA in Sydney, Australia. At NICTA, I worked on Goanna, a static analyzer for the C/C++ programming languages.

See my CV for more details.

• 16/03/2012: Today I had my last day in Aachen, I leave the Embedded Software Laboratory to work in industry.
• 06/03/2012: The slides for my presentation on automatic abstraction at the Compiler Design Lab in Saarbrücken are available here.
• 05/03/2012: The slides for my talk at the Max-Planck Institute in Saarbrücken are available from here.
• 01/03/2012: The slides for my talk at InBot'12 are available from here.
• 24/01/2012: The paper Inferring Definite Counterexamples Through Under-Approximation, which I co-authored with Axel Simon from the TU Munich, was accepted to the 4th NASA Formal Methods Symposium (NFM 2012).
• 22/11/2011: I gave an invited talk at CEA, LIST in Paris about automatic generation of abstraction for binary code. The slides are available from here.
• 15/11/2011: Today, I gave an invited talk about formal verification of PLC software at the University of Bremen. The slides are available from here.
• 03/11/2011: I gave an invited talk on automatic abstraction for bit-vector relations at the TU Vienna and the IST Austria.
• 01/09/2011: I have received a best paper award from FMICS'11 for the paper Past Time LTL Runtime Verification for Microcontroller Binary Code. The paper was co-authored Thomas Reinbacher, Martin Horauer, Andreas Steininger and Stefan Kowalewski.
• 01/08/2011: The paper Automated Test-Trace Inspection for Microcontroller Binary Code which I co-authored with Thomas Reinbacher, Daniel Schachinger and Andreas Steininger from the TU Vienna as well as Stefan Kowalewski from our group was accepted to RV'11.
• 20/07/2011: The implementation for my CAV'11 paper is available from http://www.cs.kent.ac.uk/amkdistribution.
• 03/07/2011: The paper Precise Control Flow Reconstruction Using Boolean Logic that I co-authored with Thomas Reinbacher, my colleague from TU Vienna, has been accepted to EMSOFT'11. In this paper, me and Thomas combine several techniques such as bit-blasting, my elimination algorithm from CAV and forward/backward analysis to compute fairly precise approximations of CFGs from binary code.
• 01/07/2011: The paper Adaptable Value-Set Analysis for Low-Level Code that I have co-authored with René Rydhof Hansen, Kim G. Larsen and Mads Chr. Olesen from Aalborg University as well as Stefan Kowalewski from our department was accepted for presentation at SSV'11.
• 10/06/2011: I was invited to give a talk at the MT-LAB meeting in Copenhagen. The MT-LAB is a Danish research centre for formal methods, and the talk was about my work on existential quantifier elimination.
• 06/05/2011: The paper Past Time LTL Runtime Verification for Microcontroller Binary Code that I have co-authored with Thomas Reinbacher, Martin Horauer, Andreas Steininger and Stefan Kowalewski was accepted for FMICS'11. The workshop will be held in Trento, Italy around end of August.
• 06/04/2011: We have assembled a programme committee for SSV 2011. Additionally, a call for papers is available here.
• 22/03/2011: The paper Existential Quantification as Incremental SAT which I co-authored with Andy King and Jael Kriener was accepted for CAV'11. Yeah!
• 14/03/2011: SSV 2011 will be co-located with the 2nd Conference on Interactive Theorem Proving (ITP) in Nijmegen, The Netherlands. ITP will take place from August 22 till August 25, and SSV will be held as a 2-day workshop starting the day thereafter.
• 11/03/2011: I will be visiting the group of Kim G. Larsen in Aalborg from April till June. Hence, if you need to contact me, please try via email.
• 10/02/2011: Together with Marco Roveri (FBK-IRST, Trento) and Hendrik Tews (TU Dresden), I will co-chair the 6th International Workshop on Systems Software Verification (SSV 2011).
• 09/02/2011: My paper Approximate Quantifier Elimination for Propositional Boolean Formulae co-authored with Andy King was accepted for NFM'11.
• 07/12/2010: My paper Transfer Function Synthesis without Quantifier Elimination co-authored with Andy King was accepted for ESOP'11.
• 28/10/2010: Together with Thomas Reinbacher, Martin Horauer, Andreas Steininger and Stefan Kowalewski, I received a best paper award for our contribution to MEMICS'10.
• 08/06/2010: My paper Range Analysis of Microcontroller Code using Bit-Level Congruences co-authored with Andy King and Stefan Kowalewski was accepted for FMICS'10.
• 04/05/2010: My paper Automatic Abstraction for Intervals using Boolean Formulae co-authored with Andy King was accepted for SAS'10.

• abstract interpretation of bit-vector programs (see [mc]square), in particular using automatic abstraction
• relational abstract domains
• formal verification
• software model checking
• software for embedded systems

In summary, I combine theoretical computer science with low-level programming, for example, by automatically deriving invariants for bit-twiddling binary code. I particularly enjoy utilizing SAT/SMT solvers for solving such problems. If you interested in this topic, you might want to check out my SAS'10 paper or my ESOP'11 paper, which give a good feel about how precise SAT-based abstract interpretation of bit-vector programs (such as assembly code) can get. However, to make such techniques scale, you need to apply certain other techniques, such as the projection algorithm from my CAV'11 paper.

• Symposium co-chair for the Symposium on Design & Verification Methodologies for Embedded Systems, which is a symposium within the IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications (MESA) 2012 in Suzhou, China.
• Co-chair of the 6th International Workshop on Systems Software Verification (SSV 2011) in Nijmegen, The Netherlands.
• Co-chair for the 4th Symposium on Design & Verification Tools for Embedded Systems (DVTES 2011) at IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications (MESA) 2011 in Washington DC, USA
• Program committee for the 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010) in Antwerp, Belgium
• Local organizer for the 4th International Workshop on Systems Software Verification (SSV 2009) in Aachen, Germany

We always have a number of different topics for diploma, bachelors, and masters theses in the [mc]square project. Even though I do not supervise theses myself anymore, please contact me if you are interested in working on verification in the field of embedded software, preferably via email. We can probably find an interesting topic and a supervisor.

• Ongoing
• Finished
  • Na Bai (Diploma): Dataflow Analysis for PLCs (September 2011)
  • Sebastian Biallas (Diploma): Counterexample-Guided Abstraction Refinement for Programmable Logic Controllers (April 2010)
  • Frank Birbacher (Diploma): Relational Static Analysis of IL-Programs using Congruences
  • Lucas Brutschy (B.Sc.): Static Analysis of Microcontroller Software using SAT- and Constraint-Solving (August 2009)
  • Mustafa Karafil (Diploma): Recovering Indirect Control Flow in Binary Code (August 2011)
  • Jörg Toborg (Diploma): Static Analysis for the Renesas R8C/23 Tiny Microcontroller (February 2010)

A more detailed list of my publications can be found here (including abstracts), and a list of my co-authors can be found here.

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

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

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

[BRT11]

PDF   BIB

Brauer, J., Roveri, M., and Tews, H., Eds., Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011)TU Dresden (published as technical report), 2011.

Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011)

Bibtex entry :

@proceedings { BRT11,
	editor = { Brauer, J{\"o}rg and Roveri, Marco and Tews, Hendrik },
	title = { Proceedings of the 6th International Workshop on Systems
		Software Verification (SSV 2011) },
	publisher = { TU Dresden (published as technical report) },
	isbn = { 978-3-642-19717-8 },
	year = { 2011 },
	timestamp = { 2011.12.14 },
	i11key = { editor },
	url = { https://es.fbk.eu/events/ssv2011/papers/proceedings.pdf },
	for_reporting_period = { 2011 },
}

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

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

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

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

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

• Existential Quantification as Incremental SAT. Technical University of Denmark, Copenhagen. 10-06-2011.
• Automatic Abstraction for Binary Code Verification. Aalborg University, Denmark. 13-04-2011.
• Automatic Abstraction for Intervals using Boolean Formula. Technical University of Munich, Germany. 14-05-2010.
• Static Analysis in [mc]square. University of Applied Sciences FH Technikum Vienna, Austria. 31-03-2009.

• Winter semester 2010/2011
  • Formal Methods for Embedded Systems (Lecture)
• Summer semester 2010
  • Seminar: Programmanalyse (Seminar)
• Winter semester 2009/2010
  • Formal Methods for Embedded Systems (Lecture)
  • Verification and Program Analysis (Seminar)
• Summer semester 2009
  • Applying Formal Verification Methods to Embedded Systems (Seminar)
• Winter semester 2008/2009
  • Static Analysis of Embedded Systems Software (Seminar)