Dr. rer. nat. Jörg Brauer

Contact

\|	\| Email: brauer[at]embedded[dot]rwth-aachen[dot]de “Luck favors the prepared mind.“ Louis Pasteur, 1822-1895

About me

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.

News

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.

Research Interests

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.

Professional Activities

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

B.Sc./M.Sc./Diploma Theses

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)

Publications

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

Publikations-Export

[RBH+14] PDF BIB

Reinbacher, T., Brauer, J., Horauer, M., Steininger, A., and Kowalewski, S., "Runtime verification of microcontroller binary code", Science of computer programming, vol. 80, pp. 109-129, 2014

Runtime verification of microcontroller binary code

Bibtex entry :

@article {  RBH+14,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Steininger, Andreas and Kowalewski, Stefan },
	title = { Runtime verification of microcontroller binary code },
	journal = { Science of computer programming },
	publisher = { Elsevier },
	pages = { 109-129 },
	volume = { 80 },
	year = { 2014 },
	address = { Amsterdam },
	issn = { 0167-6423 },
	organization = { Brazilian Symposium on Programming Languages },
	doi = { 10.1016/j.scico.2012.10.015 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-080463 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/231479 },
}

[RFB14] PDF BIB

Reinbacher, T., Fuegger, M., and Brauer, J., "Runtime verification of embedded real-time systems", Formal methods in system design, vol. 44, iss. 3, pp. 203-239, 2014

Runtime verification of embedded real-time systems

Bibtex entry :

@article {  RFB14,
	author = { Reinbacher, Thomas and Fuegger, Matthias and Brauer,
		J{\"o}rg },
	title = { Runtime verification of embedded real-time systems },
	journal = { Formal methods in system design },
	publisher = { Springer Science + Business Media B.V },
	pages = { 203-239 },
	volume = { 44 },
	number = { 3 },
	year = { 2014 },
	address = { Dordrecht },
	issn = { 0925-9856 },
	doi = { 10.1007/s10703-013-0199-z },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-089599 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/446689 },
}

[BK13] PDF BIB

Brauer, J. and Kowalewski, S., "Automatic abstraction for bit vectors using decision procedures", , Aachen, AIB 2013 14, 2013.

Automatic abstraction for bit vectors using decision procedures

Bibtex entry :

@techreport {  BK13,
	author = { Brauer, J{\"o}rg and Kowalewski, Stefan },
	title = { Automatic abstraction for bit vectors using decision
		procedures },
	publisher = { Fachgruppe Informatik, RWTH Aachen University },
	pages = { IV, 207 S. : graph. Darst. },
	volume = { 2013,14 },
	number = { AIB 2013 14 },
	series = { Aachener Informatik-Berichte },
	year = { 2013 },
	address = { Aachen },
	typ = { PUB:(DE-HGF)11 },
	reportid = { RWTH-CONV-010470 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/229199/files/4836.pdf },
}

[BKK13] PDF BIB

Brauer, J., King, A., and Kowalewski, S., "Abstract interpretation of microcontroller code: Intervals meet congruences", Science of computer programming, vol. 78, iss. 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 },
	publisher = { Elsevier },
	pages = { 862-883 },
	volume = { 78 },
	number = { 7 },
	year = { 2013 },
	address = { Amsterdam [u.a.] },
	issn = { 0167-6423 },
	organization = { Formal Methods for Industrial Critical Systems, 2009 },
	doi = { 10.1016/j.scico.2012.06.001 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-086725 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/238031 },
}

[KPB13] PDF BIB

Kowalewski, S., Philippou, A., and Brauer, J., "Model checking and abstract interpretation as building blocks of advanced program analysis techniques", International journal on software tools for technology transfer : STTT, vol. 15, iss. 4, pp. 287-289, 2013

Model checking and abstract interpretation as building blocks of advanced program analysis techniques

Bibtex entry :

@article {  KPB13,
	author = { Kowalewski, Stefan and Philippou, A. and Brauer, J. },
	title = { Model checking and abstract interpretation as building
		blocks of advanced program analysis techniques },
	journal = { International journal on software tools for technology
		transfer : STTT },
	publisher = { Springer },
	pages = { 287-289 },
	volume = { 15 },
	number = { 4 },
	year = { 2013 },
	address = { Berlin ; Heidelberg [u.a.] },
	issn = { 1433-2787 },
	organization = { 15th International Conference, TACAS 2009, York (UK),
		2009-03-22 - 2009-03-29 },
	doi = { 10.1007/s10009-013-0280-3 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-236324 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752289 },
}

[BBK+12] PDF BIB

Biallas, S., Brauer, J., King, A., and Kowalewski, S., "Loop Leaping with Closures", in Proc. Static Analysis : 19th International Symposium, SAS 2012, Deauville, France, September 11-13, 2012. Proceedings / edited by Antoine Miné, David Schmidt, Berlin, Heidelberg, 2012 in Lecture Notes in Computer Science, Springer, pp. 214-230.

Loop Leaping with Closures

Bibtex entry :

@inproceedings {  BBK+12,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and King, Andy and
		Kowalewski, Stefan },
	title = { Loop Leaping with Closures },
	booktitle = { Static Analysis : 19th International Symposium, SAS 2012,
		Deauville, France, September 11-13, 2012. Proceedings /
		edited by Antoine Miné, David Schmidt },
	publisher = { Springer },
	pages = { 214-230 },
	series = { Lecture Notes in Computer Science },
	year = { 2012 },
	address = { Berlin, Heidelberg },
	organization = { Static Analysis : 19th International Symposium, Deauville
		(France), 2012-09-11 - 2012-09-13 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-236335 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752305 },
}

[BBK12a] PDF BIB

Beckschulze, E., Brauer, J., and Kowalewski, S., "Access-Based Localization for Octagons", Electronic notes in theoretical computer science : ENTCS, vol. 287, pp. 29-40, 2012

Access-Based Localization for Octagons

Bibtex entry :

@article {  BBK12a,
	author = { Beckschulze, Eva and Brauer, J{\"o}rg and Kowalewski, Stefan },
	title = { Access-Based Localization for Octagons },
	journal = { Electronic notes in theoretical computer science : ENTCS },
	publisher = { Elsevier Science },
	pages = { 29-40 },
	volume = { 287 },
	year = { 2012 },
	address = { Amsterdam [u.a.] },
	issn = { 1571-0661 },
	organization = { Fourth International Workshop on Numerical and Symbolic
		Abstract Domains (France), 10-09-2012 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-043099 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/165238 },
}

[BBK12b] PDF BIB

Biallas, S., Brauer, J., and Kowalewski, S., "Arcade.PLC : a Verification Platform for Programmable Logic Controllers", in Proc. 2012 proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering (ASE 2012) : Essen, Germany, 3 - 7 September 2012, Piscataway, NJ, 2012, IEEE, 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 = { 2012 proceedings of the 27th IEEE/ACM International
		Conference on Automated Software Engineering (ASE 2012) :
		Essen, Germany, 3 - 7 September 2012 },
	publisher = { IEEE },
	pages = { 338-341 },
	year = { 2012 },
	address = { Piscataway, NJ },
	organization = { 27th IEEE/ACM International Conference on Automated Software
		Engineering, Essen (Germany), 2012-09-03 - 2012-09-07 },
	doi = { 10.1145/2351676.2351741 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-170936 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/97761 },
}

[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) [Elektronische Ressource] / Hrsg.: Jörg Brauer ; Marco Roveri ; Hendrik Tews, Wadern, 2012 in OASIcs - OpenAccess Series in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für 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) [Elektronische Ressource] / Hrsg.: J{\"o}rg
		Brauer ; Marco Roveri ; Hendrik Tews },
	publisher = { Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik },
	pages = { 32-43 },
	series = { OASIcs - OpenAccess Series in Informatics },
	year = { 2012 },
	address = { Wadern },
	doi = { 10.4230/OASIcs.SSV.2011.32 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-198838 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/128784 },
}

[BK12a] PDF BIB

Brauer, J. and King, A., "Transfer function synthesis without quantifier elimination", Logical methods in computer science : LMCS, vol. 8, iss. 3, 2012

Transfer function synthesis without quantifier elimination

Bibtex entry :

@article {  BK12a,
	author = { Brauer, J{\"o}rg and King, Andy },
	title = { Transfer function synthesis without quantifier elimination },
	journal = { Logical methods in computer science : LMCS },
	publisher = { Department of Theoretical Computer Science, TU [u.a.] },
	volume = { 8 },
	number = { 3 },
	year = { 2012 },
	address = { Braunschweig },
	issn = { 1860-5974 },
	doi = { 10.2168/LMCS-8(3:17)2012 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-079893 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/218122/files/218122.pdf },
}

[BS12] PDF BIB

Brauer, J. and Simon, A., "Inferring Definite Counterexamples Through Under-Approximation", in Proc. NASA formal methods : 4th international symposium, NFM 2012, Norfolk, VA, USA, April 3 - 5, 2012 ; proceedings / Alwyn E. Goodloe; Suzette Person (ed.), Berlin ; Heidelberg [u.a.], 2012 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 : 4th international symposium, NFM 2012,
		Norfolk, VA, USA, April 3 - 5, 2012 ; proceedings / Alwyn E.
		Goodloe; Suzette Person (ed.) },
	publisher = { Springer },
	pages = { 54-69 },
	series = { Lecture Notes in Computer Science },
	year = { 2012 },
	address = { Berlin ; Heidelberg [u.a.] },
	organization = { NASA formal methods : 4th international symposium, Norfolk,
		VA (USA), 2012-04-03 - 2012-04-05 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-194497 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/123648 },
}

[BSK12] PDF BIB

Brauer, J., Schlich, B., and Kowalewski, S., "Parallel and distributed invariant checking of microcontroller software", Electronic notes in theoretical computer science : ENTCS, vol. 287, pp. 45-63, 2012

Parallel and distributed invariant checking of microcontroller software

Bibtex entry :

@article {  BSK12,
	author = { Brauer, J{\"o}rg and Schlich, Bastian and Kowalewski, Stefan },
	title = { Parallel and distributed invariant checking of
		microcontroller software },
	journal = { Electronic notes in theoretical computer science : ENTCS },
	publisher = { Elsevier Science },
	pages = { 45-63 },
	volume = { 287 },
	year = { 2012 },
	address = { Amsterdam [u.a.] },
	issn = { 1571-0661 },
	organization = { Fourth International Workshop on Numerical and Symbolic
		Abstract Domains (France), 10-09-2010 },
	doi = { 10.1016/j.entcs.2009.09.059 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-013643 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/132534 },
}

[BBK+11] PDF BIB

Biallas, S., Brauer, J., Kowalewski, S., and Schlich, B., "Automatically Deriving Symbolic Invariants for PLC Programs Written in IL", in Proc. Formal methods for automation and safety in railway and automotive systems : FORMS/FORMAT 2010 ; [8th symposium ; proceedings] / Eckehard Schnieder; Géza Tarnai, eds., Heidelberg [u.a.], 2011, Springer, pp. 237-245.

Automatically Deriving Symbolic Invariants for PLC Programs Written in IL

Bibtex entry :

@inproceedings {  BBK+11,
	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 = { Formal methods for automation and safety in railway and
		automotive systems : FORMS/FORMAT 2010 ; [8th symposium ;
		proceedings] / Eckehard Schnieder; Géza Tarnai, eds. },
	publisher = { Springer },
	pages = { 237-245 },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-14261-1 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-196797 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/126461 },
}

[BBK11] PDF BIB

Biallas, S., Brauer, J., and Kowalewski, S., "SAT-Based Abstraction Refinement for Programmable Logic Controllers", in Proc. 3rd International Workshop on Dependable Control of Discrete Systems 2011, DCDS 2011, Saarbrücken, Germany, 15th-17theJune 2011, Piscataway, NJ, 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 = { 3rd International Workshop on Dependable Control of Discrete
		Systems 2011, DCDS 2011, Saarbr{\"u}cken, Germany,
		15th-17theJune 2011 },
	publisher = { IEEE },
	pages = { 96-101 },
	year = { 2011 },
	address = { Piscataway, NJ },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-194508 },
	cin = { 122810 / 120000 },
	url = { http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=05970325 },
}

[BBS+11] 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) : 28 - 31 March 2011, Newport Beach, California, USA ; proceedings, Piscataway, NJ, 2011, IEEE, pp. 33-40.

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

Bibtex entry :

@inproceedings {  BBS+11,
	author = { Beckschulze, Eva and Brauer, J{\"o}rg and Stollenwerk,
		André 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) : 28 - 31 March 2011, Newport
		Beach, California, USA ; proceedings },
	publisher = { IEEE },
	pages = { 33-40 },
	year = { 2011 },
	address = { Piscataway, NJ },
	organization = { 14th IEEE International Symposium on
		Object/Component/Service-Oriented Real-Time Distributed
		Computing, Newport Beach, CA (USA), 2011-03-28 - 2011-08-31 },
	doi = { 10.1109/ISORCW.2011.40 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-194737 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/124002 },
}

[BK11] PDF BIB

Brauer, J. and King, A., "Approximate Quantifier Elimination for Propositional Boolean Formulae", in Proc. NASA formal methods : third international symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011 ; proceedings / Mihaela Bobaru ... (eds.), Heidelberg [u.a.], 2011 in Lecture Notes in Computer Science, Springer, pp. 73-88.

Approximate Quantifier Elimination for Propositional Boolean Formulae

Bibtex entry :

@inproceedings {  BK11,
	author = { Brauer, J{\"o}rg and King, Andy },
	title = { Approximate Quantifier Elimination for Propositional Boolean
		Formulae },
	booktitle = { NASA formal methods : third international symposium, NFM
		2011, Pasadena, CA, USA, April 18-20, 2011 ; proceedings /
		Mihaela Bobaru ... (eds.) },
	publisher = { Springer },
	pages = { 73-88 },
	series = { Lecture Notes in Computer Science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-20398-5 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-194773 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/124043 },
}

[BK11a] PDF BIB

Brauer, J. and King, A., "Transfer Function Synthesis without Quantifier Elimination", in Proc. Programming languages and systems : 20th European Symposium on Programming, ESOP 2011, held as part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011 ; proceedings / Gilles Barthe (ed.), Heidelberg [u.a.], 2011 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 = { Programming languages and systems : 20th European Symposium
		on Programming, ESOP 2011, held as part of the Joint
		European Conference on Theory and Practice of Software,
		ETAPS 2011, Saarbr{\"u}cken, Germany, March 26-April 3, 2011
		; proceedings / Gilles Barthe (ed.) },
	publisher = { Springer },
	pages = { 97-115 },
	series = { Lecture notes in computer science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-19718-5 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-196794 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/126458 },
}

[BKK11] PDF BIB

Brauer, J., King, A., and Kriener, J., "Existential Quantification as Incremental SAT", in Proc. Computer aided verification : 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011 ; proceedings / Ganesh Gopalakrishnan; Shaz Qadeer (eds.), Heidelberg [u.a.], 2011 in Lecture notes in computer science, Springer, pp. 191-207.

Existential Quantification as Incremental SAT

Bibtex entry :

@inproceedings {  BKK11,
	author = { Brauer, J{\"o}rg and King, Andy and Kriener, Jael },
	title = { Existential Quantification as Incremental SAT },
	booktitle = { Computer aided verification : 23rd international conference,
		CAV 2011, Snowbird, UT, USA, July 14-20, 2011 ; proceedings
		/ Ganesh Gopalakrishnan; Shaz Qadeer (eds.) },
	publisher = { Springer },
	pages = { 191-207 },
	series = { Lecture notes in computer science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-22110-1 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-196588 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/126209 },
}

[BRT11] PDF BIB

Brauer, J., Roveri, M., and Tews, H., "Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011)", , Dresden, TUD-FI11-02-August 2011, 2011.

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

Bibtex entry :

@techreport {  BRT11,
	author = { 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 },
	pages = { 101 S. },
	number = { TUD-FI11-02-August 2011 },
	year = { 2011 },
	address = { Dresden },
	typ = { PUB:(DE-HGF)26 },
	reportid = { RWTH-CONV-008161 },
	cin = { 122810 / 120000 },
	url = { https://es.fbk.eu/events/ssv2011/papers/proceedings.pdf },
}

[RB11] PDF BIB

Reinbacher, T. and Brauer, J., "Precise Control Flow Reconstruction Using Boolean Logic", in Proc. EMSOFT '11 : Proceedings of the ninth ACM international conference on Embedded software ; October 9-14, 2011, Taipei, Taiwan, New York, NY, 2011, ACM, pp. 117-126.

Precise Control Flow Reconstruction Using Boolean Logic

Bibtex entry :

@inproceedings {  RB11,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg },
	title = { Precise Control Flow Reconstruction Using Boolean Logic },
	booktitle = { EMSOFT '11 : Proceedings of the ninth ACM international
		conference on Embedded software ; October 9-14, 2011,
		Taipei, Taiwan },
	publisher = { ACM },
	pages = { 117-126 },
	year = { 2011 },
	address = { New York, NY },
	doi = { 10.1145/2038642.2038662 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-198496 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/128379 },
}

[RBH+11] PDF BIB

Reinbacher, T., Brauer, J., Horauer, M., Steininger, A., and Kowalewski, S., "Past Time LTL Runtime Verification for Microcontroller Binary Code", in Proc. Formal methods for industrial critical systems : 16th international workshop, FMICS 2011, Trento, Italy, August 29 - 30, 2011 ; proceedings / Gwen Salaün; Bernhard Schätz (eds.), Heidelberg [u.a.], 2011 in Lecture notes in computer science, Springer, pp. 37-51.

Past Time LTL Runtime Verification for Microcontroller Binary Code

Bibtex entry :

@inproceedings {  RBH+11,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Steininger, Andreas and Kowalewski, Stefan },
	title = { Past Time LTL Runtime Verification for Microcontroller
		Binary Code },
	booktitle = { Formal methods for industrial critical systems : 16th
		international workshop, FMICS 2011, Trento, Italy, August 29
		- 30, 2011 ; proceedings / Gwen Sala{\"u}n; Bernhard
		Sch{\"a}tz (eds.) },
	publisher = { Springer },
	pages = { 37-51 },
	series = { Lecture notes in computer science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-24431-5 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-194606 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/123834 },
}

[RBS+11] PDF BIB

Reinbacher, T., Brauer, J., Schachinger, D., Steininger, A., and Kowalewski, S., "Automated Test-Trace Inspection for Microcontroller Binary Code", in Proc. Runtime Verification : Second International Conference, RV 2011, San Francisco, CA, USA, September 27-30, 2011, Revised Selected Papers / edited by Sarfraz Khurshid, Koushik Sen, Berlin ; Heidelberg, 2011 in Lecture notes in computer science, 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 = { Runtime Verification : Second International Conference, RV
		2011, San Francisco, CA, USA, September 27-30, 2011, Revised
		Selected Papers / edited by Sarfraz Khurshid, Koushik Sen },
	publisher = { Springer },
	pages = { 239-244 },
	series = { Lecture notes in computer science },
	year = { 2011 },
	address = { Berlin ; Heidelberg },
	doi = { 10.1007/978-3-642-29860-8_18 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-194496 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/123647 },
}

[RHS+11] 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 convergence, vol. 1, iss. 2, pp. 186-205, 2011

Model checking embedded software of an industrial knitting machine

Bibtex entry :

@article {  RHS+11,
	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 convergence },
	publisher = { Inderscience Publishers },
	pages = { 186-205 },
	volume = { 1 },
	number = { 2 },
	year = { 2011 },
	address = { Geneva },
	issn = { 2042-3217 },
	doi = { 10.1504/IJITCC.2011.039285 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-052838 },
	cin = { 122810 / 120000 },
	url = { http://www.inderscience.com/IJITCC },
}

[RSM+11] PDF 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. Proceedings of the ASME International Design Engineering Technical Conferences and Computers and Information in Engineering Conference - 2011 : presented at ASME 2011 International Design Engineering Technical Conferences and Computers and Information in Engineering Conference, August 28 - 31, 2011, Washington, D.C. / sponsored by the Design Engineering Division, ASME; the Computers and Information in Engineering Division, ASME. - Vol. 3: ASME/IEEE International Conference on Mechatronic and Embedded Systems and Applications, Pt. A, New York, NY, 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 = { Proceedings of the ASME International Design Engineering
		Technical Conferences and Computers and Information in
		Engineering Conference - 2011 : presented at ASME 2011
		International Design Engineering Technical Conferences and
		Computers and Information in Engineering Conference, August
		28 - 31, 2011, Washington, D.C. / sponsored by the Design
		Engineering Division, ASME; the Computers and Information in
		Engineering Division, ASME. - Vol. 3: ASME/IEEE
		International Conference on Mechatronic and Embedded Systems
		and Applications, Pt. A },
	publisher = { ASME },
	pages = { 3-12 },
	year = { 2011 },
	address = { New York, NY },
	doi = { 10.1115/DETC2011-47139 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-195986 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/125522 },
}

[SBK11] PDF BIB

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

Application of Static Analyses for State-Space Reduction to the 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
		the Microcontroller Binary Code },
	journal = { Science of computer programming },
	publisher = { Elsevier },
	pages = { 100-118 },
	volume = { 76 },
	number = { 2 },
	year = { 2011 },
	address = { Amsterdam [u.a.] },
	issn = { 0167-6423 },
	doi = { 10.1016/j.scico.2010.03.006 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-062661 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/186222 },
}

[SNB+11] PDF BIB

Schlich, B., Noll, T., Brauer, J., and Brutschy, L., "Reduction of Interrupt Handler Executions for Model Checking Embedded Software", in Proc. Hardware and software: verification and testing : 5th International Haifa Verification Conference, HCV 2009, Haifa, Israel, October 19-22, 2009 : revised selected papers / Kedar Namjoshi ... (eds.), Heidelberg [u.a.], 2011 in Lecture Notes in Computer Science, Springer.

Reduction of Interrupt Handler Executions for Model Checking Embedded Software

Bibtex entry :

@inproceedings {  SNB+11,
	author = { Schlich, Bastian and Noll, Thomas and Brauer, J{\"o}rg and
		Brutschy, Lucas },
	title = { Reduction of Interrupt Handler Executions for Model Checking
		Embedded Software },
	booktitle = { Hardware and software: verification and testing : 5th
		International Haifa Verification Conference, HCV 2009,
		Haifa, Israel, October 19-22, 2009 : revised selected papers
		/ Kedar Namjoshi ... (eds.) },
	publisher = { Springer },
	series = { Lecture Notes in Computer Science },
	year = { 2011 },
	address = { Heidelberg [u.a.] },
	doi = { 10.1007/978-3-642-19237-1_5 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-187757 },
	cin = { 122810 / 121310 / 120000 },
	url = { http://publications.rwth-aachen.de/record/116214 },
}

[BBG+10] PDF BIB

Biallas, S., Brauer, J., Gückel, D., and Kowalewski, S., "On-The-Fly Path Reduction", in Proc. 4th International Workshop on Harnessing Theories for Tool Support in Software : TTSS’10 ; East China Normal University, Shanghai, China, November 15, 2010 ; Preliminary Proceedings / Eds.: Min Zhang and Volker Stolz, Macau, 2010 in UNU-IIST Report, UNU-IIST, pp. 108-122.

On-The-Fly Path Reduction

Bibtex entry :

@inproceedings {  BBG+10,
	author = { Biallas, Sebastian and Brauer, J{\"o}rg and G{\"u}ckel,
		Dominique and Kowalewski, Stefan },
	title = { On-The-Fly Path Reduction },
	booktitle = { 4th International Workshop on Harnessing Theories for Tool
		Support in Software : TTSS’10 ; East China Normal
		University, Shanghai, China, November 15, 2010 ; Preliminary
		Proceedings / Eds.: Min Zhang and Volker Stolz },
	publisher = { UNU-IIST },
	pages = { 108-122 },
	series = { UNU-IIST Report },
	year = { 2010 },
	address = { Macau },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190152 },
	cin = { 122810 / 120000 },
	url = { http://i.unu.edu/unu/u/publication/000/001/286/report444.pdf },
}

[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, 2010.

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 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-189856 },
	cin = { 122810 / 120000 },
	url = { http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bbk10.pdf },
}

[BK10] PDF BIB

Brauer, J. and King, A., "Automatic Abstraction for Intervals using Boolean Formulae", in Proc. Static analysis : 17th international symposium, SAS 2010, Perpignan, France, September 14-16, 2010 ; proceedings / Radhia Cousot; Matthieu Martel (eds.), Berlin [u.a.], 2010 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 : 17th international symposium, SAS 2010,
		Perpignan, France, September 14-16, 2010 ; proceedings /
		Radhia Cousot; Matthieu Martel (eds.) },
	publisher = { Springer },
	pages = { 167-183 },
	series = { Lecture notes in computer science },
	year = { 2010 },
	address = { Berlin [u.a.] },
	doi = { 10.1007/978-3-642-15769-1_11 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190302 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/119140 },
}

[BKK+10] PDF BIB

Brauer, J., Kamin, V., Kowalewski, S., and Noll, T., "Loop Refinement using Octagons and Satisfiability", in Proc. SSV'10 : Proceedings of the 5th international conference on Systems software verification, New York, NY, 2010, ACM, p. 9.

Loop Refinement using Octagons and Satisfiability

Bibtex entry :

@inproceedings {  BKK+10,
	author = { Brauer, J{\"o}rg and Kamin, Volker and Kowalewski, Stefan
		and Noll, Thomas },
	title = { Loop Refinement using Octagons and Satisfiability },
	booktitle = { SSV'10 : Proceedings of the 5th international conference on
		Systems software verification },
	publisher = { ACM },
	pages = { 9 S. },
	year = { 2010 },
	address = { New York, NY },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-196798 },
	cin = { 122810 / 121310 / 120000 },
	url = { http://dl.acm.org/citation.cfm?id=1929004&picked=prox },
}

[BKK10] PDF 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 : 15th international workshop, FMICS 2010, Antwerp, Belgium, September 20 - 21, 2010 ; proceedings / Stefan Kowalewski; Marco Roveri (eds.), Berlin [u.a.], 2010 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 : 15th
		international workshop, FMICS 2010, Antwerp, Belgium,
		September 20 - 21, 2010 ; proceedings / Stefan Kowalewski;
		Marco Roveri (eds.) },
	publisher = { Springer },
	pages = { 82-98 },
	series = { Lecture notes in computer science },
	year = { 2010 },
	address = { Berlin [u.a.] },
	doi = { 10.1007/978-3-642-15898-8_6 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190303 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/119141 },
}

[BNS10] PDF BIB

Brauer, J., Noll, T., and Schlich, B., "Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software", in Proc. SCOPES '10 Proceedings of the 13th International Workshop on Software & Compilers for Embedded Systems : St. Goar, Germany - June 29-30, 2010, New York, NY, 2010 in ACM Digital Library, 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 = { SCOPES '10 Proceedings of the 13th International Workshop on
		Software & Compilers for Embedded Systems : St. Goar,
		Germany - June 29-30, 2010 },
	publisher = { ACM },
	series = { ACM Digital Library },
	year = { 2010 },
	address = { New York, NY },
	doi = { 10.1145/1811212.1811216 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-191119 },
	cin = { 122810 / 121310 / 120000 },
	url = { http://publications.rwth-aachen.de/record/120063 },
}

[GBK10] PDF BIB

Gückel, D., Brauer, J., and Kowalewski, S., "A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification", in Proc. 2010 International Symposium on Industrial Embedded Systems (SIES 2010) : Trento, Italy, 7 - 9 July 2010 / [University of Trento, Italy; IEEE; IES], Piscataway, NJ, 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 },
	title = { A System for Synthesizing Abstraction-Enabled Simulators for
		Binary Code Verification },
	booktitle = { 2010 International Symposium on Industrial Embedded Systems
		(SIES 2010) : Trento, Italy, 7 - 9 July 2010 / [University
		of Trento, Italy; IEEE; IES] },
	publisher = { IEEE },
	pages = { 118-127 },
	year = { 2010 },
	address = { Piscataway, NJ },
	doi = { 10.1109/SIES.2010.5551382 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190384 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/119226 },
}

[GSB+10] PDF BIB

Gückel, D., Schlich, B., Brauer, J., and Kowalewski, S., "Synthesizing Simulators for Model Checking Microcontroller Binary", in Proc. Proceedings of the 13th IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems : April 14–16, 2010, Vienna, Austria / Sponsored by IEEE Computer Society, Test Technology Techn. Council, In coop. with Dept. of Computer Engineering, Fac. of Informatics, Vienna Univ. of Techn., Piscataway, NJ, 2010, IEEE, pp. 313-316.

Synthesizing Simulators for Model Checking Microcontroller Binary

Bibtex entry :

@inproceedings {  GSB+10,
	author = { G{\"u}ckel, Dominique and Schlich, Bastian and Brauer,
		J{\"o}rg and Kowalewski, Stefan },
	title = { Synthesizing Simulators for Model Checking Microcontroller
		Binary },
	booktitle = { Proceedings of the 13th IEEE Symposium on Design and
		Diagnostics of Electronic Circuits and Systems : April
		14–16, 2010, Vienna, Austria / Sponsored by IEEE Computer
		Society, Test Technology Techn. Council, In coop. with Dept.
		of Computer Engineering, Fac. of Informatics, Vienna Univ.
		of Techn. },
	publisher = { IEEE },
	pages = { 313-316 },
	year = { 2010 },
	address = { Piscataway, NJ },
	doi = { 10.1109/DDECS.2010.5491761 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-190385 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/119227 },
}

[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 (Selected Papers) (MEMICS 2010) [Elektronische Ressource] / Hrsg.: Ludek Matyska ; Michal Kozubek ; Tomáš Vojnar ; Pavel Zemcík ; David Antos, Wadern, 2010 in OASIcs - OpenAccess Series in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 101-108.

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 (Selected Papers) (MEMICS 2010)
		[Elektronische Ressource] / Hrsg.: Ludek Matyska ; Michal
		Kozubek ; Tomáš Vojnar ; Pavel Zemcík ; David Antos },
	publisher = { Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik },
	pages = { 101-108 },
	series = { OASIcs - OpenAccess Series in Informatics },
	year = { 2010 },
	address = { Wadern },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-196795 },
	cin = { 120000 / 122810 },
	url = { http://publications.rwth-aachen.de/record/126459 },
}

[BHS09] PDF BIB

Brauer, J., Huuck, R., and Schlich, B., "Interprocedural pointer analysis in Goanna", Electronic notes in theoretical computer science : ENTCS, vol. 254, pp. 65-83, 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 : ENTCS },
	publisher = { Elsevier Science },
	pages = { 65-83 },
	volume = { 254 },
	year = { 2009 },
	address = { Amsterdam [u.a.] },
	issn = { 1571-0661 },
	doi = { 10.1016/j.entcs.2009.09.060 },
	typ = { PUB:(DE-HGF)16 },
	reportid = { RWTH-CONV-013641 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/132532 },
}

[BSR+09] PDF BIB

Brauer, J., Schlich, B., Reinbacher, T., and Kowalewski, S., "Stack bounds analysis of microcontroller assembly code", in Proc. Embedded Systems Week 2009 : CODES+ISSS’09, CASES’09, EMSOFT’09 ; Proceedings of the 2009 international conference on Compilers, architecture, and synthesis for embedded systems ; 2009, Grenoble, France, October 11 - 16, 2009, New York, NY, 2009, ACM Press.

Stack bounds analysis of microcontroller assembly code

Bibtex entry :

@inproceedings {  BSR+09,
	author = { Brauer, J{\"o}rg and Schlich, Bastian and Reinbacher, Thomas
		and Kowalewski, Stefan },
	title = { Stack bounds analysis of microcontroller assembly code },
	booktitle = { Embedded Systems Week 2009 : CODES+ISSS’09, CASES’09,
		EMSOFT’09 ; Proceedings of the 2009 international
		conference on Compilers, architecture, and synthesis for
		embedded systems ; 2009, Grenoble, France, October 11 - 16,
		2009 },
	publisher = { ACM Press },
	year = { 2009 },
	address = { New York, NY },
	doi = { 10.1145/1631716.1631721 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-173253 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/100433 },
}

[RBH+09] PDF BIB

Reinbacher, T., Brauer, J., Horauer, M., and Schlich, B., "Refining assembly code static analysis for the Intel MCS-51 microcontroller", in Proc. 2009 IEEE International Symposium on Industrial Embedded Systems (SIES 2009) : Lausanne, Switzerland, 08 - 10 July 2009 / [sponsored by: IEEE Industrial Electronics Society (IES)]), Piscataway, NJ, 2009, IEEE, pp. 161-170.

Refining assembly code static analysis for the Intel MCS-51 microcontroller

Bibtex entry :

@inproceedings {  RBH+09,
	author = { Reinbacher, Thomas and Brauer, J{\"o}rg and Horauer, Martin
		and Schlich, Bastian },
	title = { Refining assembly code static analysis for the Intel MCS-51
		microcontroller },
	booktitle = { 2009 IEEE International Symposium on Industrial Embedded
		Systems (SIES 2009) : Lausanne, Switzerland, 08 - 10 July
		2009 / [sponsored by: IEEE Industrial Electronics Society
		(IES)]) },
	publisher = { IEEE },
	pages = { 161-170 },
	year = { 2009 },
	address = { Piscataway, NJ },
	doi = { 10.1109/SIES.2009.5196212 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-172391 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/99425 },
}

[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. Proceedings of the 2009 Fourth International Conference on Embedded and Multimedia Computing : EM-Com 2009 : [December 10-12, 2009, Jeju Island, Korea], Piscataway, NJ, 2009, IEEE, p. 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 = { Proceedings of the 2009 Fourth International Conference on
		Embedded and Multimedia Computing : EM-Com 2009 : [December
		10-12, 2009, Jeju Island, Korea] },
	publisher = { IEEE },
	pages = { 8 S. },
	year = { 2009 },
	address = { Piscataway, NJ },
	doi = { 10.1109/EM-COM.2009.5402986 },
	typ = { PUB:(DE-HGF)8 },
	reportid = { RWTH-CONV-199048 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/129021 },
}

[SBW+09] 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 {  SBW+09,
	author = { Schlich, Bastian and Brauer, J{\"o}rg and Wernerus, J{\"o}rg
		and Kowalewski, Stefan },
	title = { Direct Model Checking of {PLC} Programs in {IL} },
	booktitle = { Dependable Control of Discrete Systems (DCDS'09), Bari,
		Italy },
	pages = { 28-33 },
	year = { 2009 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-236337 },
	cin = { 122810 / 120000 },
	url = { http://publications.rwth-aachen.de/record/752318 },
}

[HFS+08] PDFBIB

Huuck, R., Fehnker, A., Seefried, S., and Brauer, J., "Goanna: syntactic software model checking", in Proc. Automated technology for verification and analysis : 6th international symposium, ATVA 2008, Seoul, Korea, October 20 - 23, 2008 ; proceedings / Sungdeok (Steve) Cha; Jin-Young Choi; Moonzoo Kim; Insup Lee; Mahesh Viswanathan (eds.), Berlin [u.a.], 2008 in Lecture notes in computer science, Springer, pp. 216-221.

Goanna: syntactic software model checking

Bibtex entry :

@inproceedings {  HFS+08,
	author = { Huuck, Ralf and Fehnker, Ansgar and Seefried, Sean and
		Brauer, J{\"o}rg },
	title = { Goanna: syntactic software model checking },
	booktitle = { Automated technology for verification and analysis : 6th
		international symposium, ATVA 2008, Seoul, Korea, October 20
		- 23, 2008 ; proceedings / Sungdeok (Steve) Cha; Jin-Young
		Choi; Moonzoo Kim; Insup Lee; Mahesh Viswanathan (eds.) },
	publisher = { Springer },
	pages = { 216-221 },
	series = { Lecture notes in computer science },
	year = { 2008 },
	address = { Berlin [u.a.] },
	organization = { 6th International Symposium on Automated Technology for
		Verification and Analysis, Seoul (South Korea), 2008-10-20 -
		2008-10-23 },
	doi = { 10.1007/978-3-540-88387-6_17 },
	typ = { PUB:(DE-HGF)7 },
	reportid = { RWTH-CONV-095469 },
}

Invited Talks

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.

Teaching

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)

Chair of CS 11

Research

Tools

Teaching

Events

Dr. rer. nat. Jörg Brauer

Contact

About me

News

Research Interests

Professional Activities

B.Sc./M.Sc./Diploma Theses

Publications

Runtime verification of microcontroller binary code

Bibtex entry :

Runtime verification of embedded real-time systems

Bibtex entry :

Automatic abstraction for bit vectors using decision procedures

Bibtex entry :

Abstract interpretation of microcontroller code: Intervals meet congruences

Bibtex entry :

Model checking and abstract interpretation as building blocks of advanced program analysis techniques

Bibtex entry :

Loop Leaping with Closures

Bibtex entry :

Access-Based Localization for Octagons

Bibtex entry :

Arcade.PLC : a Verification Platform for Programmable Logic Controllers

Bibtex entry :

Adaptable Value-Set Analysis for Low-Level Code

Bibtex entry :

Transfer function synthesis without quantifier elimination

Bibtex entry :

Inferring Definite Counterexamples Through Under-Approximation

Bibtex entry :

Parallel and distributed invariant checking of microcontroller software

Bibtex entry :

Automatically Deriving Symbolic Invariants for PLC Programs Written in IL

Bibtex entry :

SAT-Based Abstraction Refinement for Programmable Logic Controllers

Bibtex entry :

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

Bibtex entry :

Approximate Quantifier Elimination for Propositional Boolean Formulae

Bibtex entry :

Transfer Function Synthesis without Quantifier Elimination

Bibtex entry :

Existential Quantification as Incremental SAT

Bibtex entry :

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

Bibtex entry :

Precise Control Flow Reconstruction Using Boolean Logic

Bibtex entry :

Past Time LTL Runtime Verification for Microcontroller Binary Code

Bibtex entry :

Automated Test-Trace Inspection for Microcontroller Binary Code

Bibtex entry :

Model checking embedded software of an industrial knitting machine

Bibtex entry :

Hardware Support for Efficient Testing of Embedded Software

Bibtex entry :

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

Bibtex entry :

Reduction of Interrupt Handler Executions for Model Checking Embedded Software

Bibtex entry :

On-The-Fly Path Reduction

Bibtex entry :

Counterexample-Guided Abstraction Refinement for PLCs

Bibtex entry :

Automatic Abstraction for Intervals using Boolean Formulae

Bibtex entry :

Loop Refinement using Octagons and Satisfiability

Bibtex entry :

Range Analysis of Microcontroller Code using Bit-Level Congruences

Bibtex entry :

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

Bibtex entry :

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

Bibtex entry :

Synthesizing Simulators for Model Checking Microcontroller Binary