====== Dr. rer. nat. Jörg Brauer ======
~~NOTOC~~
~~NOCACHE~~
===== Contact =====

{|
|-
||{{:lehrstuhl:mitarbeiter:brauer.jpg|}}
||
Email: brauer[at]embedded[dot]rwth-aachen[dot]de
\\
\\
<quote>"//Luck favors the prepared mind.//"\\
Louis Pasteur, 1822-1895</quote>
|}

===== About me =====

I moved to Bremen.
\\
\\
Prior to moving up north, I used to be a PhD student heading the [[http://www.embedded.rwth-aachen.de/mc_square|[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 [[http://ti.tuwien.ac.at/ecs/research/projects/cevtes|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 [[http://www.nicta.com.au|NICTA]] in Sydney, Australia. At NICTA, I worked on [[http://www.nicta.com.au/research/projects/goanna/|Goanna]], a static analyzer for the C/C++ programming languages.
\\
\\
See {{:en:lehrstuhl:mitarbeiter:brauer:cv_brauer.pdf|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 [[http://rw4.cs.uni-saarland.de/index.shtml|Compiler Design Lab]] in Saarbrücken are available {{:en:lehrstuhl:mitarbeiter:brauer:saarbruecken_2012_slides.pdf|here}}.
  * **05/03/2012:** The slides for my talk at the Max-Planck Institute in Saarbrücken are available from {{:en:lehrstuhl:mitarbeiter:brauer:mpi_2012_slides.pdf|here}}.
  * **01/03/2012:** The slides for my talk at [[http://inbot.mwcollect.org|InBot'12]] are available from {{:en:lehrstuhl:mitarbeiter:brauer:inbot_2012_slides.pdf|here}}.
  * **24/01/2012:** The paper [[http://www.embedded.rwth-aachen.de/lib/exe/fetch.php?media=bib:bs12.pdf|Inferring Definite Counterexamples Through Under-Approximation]], which I co-authored with [[http://www2.in.tum.de/hp/Main?nid=130|Axel Simon]] from the TU Munich, was accepted to the [[http://shemesh.larc.nasa.gov/nfm2012/|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 {{:en:lehrstuhl:mitarbeiter:brauer:paris_2011_slides.pdf|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 {{:en:lehrstuhl:mitarbeiter:brauer:bremen_2011_slides.pdf|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 [[http://events.fortiss.org/fmics2011/|FMICS'11]] for the paper {{:bib:rbh11.pdf|Past Time LTL Runtime Verification for Microcontroller Binary Code}}. The paper was co-authored [[http://ti.tuwien.ac.at/ecs/people/treinbacher|Thomas Reinbacher]], [[http://embsys.technikum-wien.at/staff/horauer/index.php|Martin Horauer]], [[http://ti.tuwien.ac.at/ecs/people/steininger|Andreas Steininger]] and [[:en:lehrstuhl:mitarbeiter:kowalewski|Stefan Kowalewski]].
  * **01/08/2011:** The paper //Automated Test-Trace Inspection for Microcontroller Binary Code// which I co-authored with [[http://ti.tuwien.ac.at/ecs/people/treinbacher|Thomas Reinbacher]], Daniel Schachinger and [[http://ti.tuwien.ac.at/ecs/people/steininger|Andreas Steininger]] from the TU Vienna as well as [[:en:lehrstuhl:mitarbeiter:kowalewski|Stefan Kowalewski]] from our group was accepted to [[http://rv2011.eecs.berkeley.edu/Home.html|RV'11]].
  * **20/07/2011:** The implementation for my {{:bib:bkk11a.pdf|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 [[http://ti.tuwien.ac.at/ecs/people/treinbacher|Thomas Reinbacher]], my colleague from TU Vienna, has been accepted to [[http://www.emsoft.org/|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 [[http://www.cs.aau.dk/~rrh/|René Rydhof Hansen]], [[http://www.cs.aau.dk/~kgl/|Kim G. Larsen]] and Mads Chr. Olesen from Aalborg University as well as [[:en:lehrstuhl:mitarbeiter:kowalewski|Stefan Kowalewski]] from our department was accepted for presentation at [[https://es.fbk.eu/events/ssv2011|SSV'11]].
  * **10/06/2011:** I was invited to give a talk at the [[http://www.mt-lab.dk/|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 {{:bib:rbh11.pdf|Past Time LTL Runtime Verification for Microcontroller Binary Code}} that I have co-authored with [[http://ti.tuwien.ac.at/ecs/people/treinbacher|Thomas Reinbacher]], [[http://embsys.technikum-wien.at/staff/horauer/index.php|Martin Horauer]], [[http://ti.tuwien.ac.at/ecs/people/steininger|Andreas Steininger]] and [[:en:lehrstuhl:mitarbeiter:kowalewski|Stefan Kowalewski]] was accepted for [[http://events.fortiss.org/fmics2011/|FMICS'11]]. The workshop will be held in Trento, Italy around end of August.
  * **06/04/2011:** We have assembled a [[https://es.fbk.eu/events/ssv2011/pc.php|programme committee]] for [[https://es.fbk.eu/events/ssv2011|SSV 2011]]. Additionally, a call for papers is available [[https://es.fbk.eu/events/ssv2011/cfp/ssv2011-cfpaper.txt|here]].
  * **22/03/2011:** The paper {{:bib:bkk11a.pdf|Existential Quantification as Incremental SAT}} which I co-authored with [[http://www.cs.kent.ac.uk/people/staff/amk/|Andy King]] and [[http://www.cs.kent.ac.uk/people/rpg/jek26/|Jael Kriener]] was accepted for [[http://www.cs.utah.edu/events/conferences/cav2011/|CAV'11]]. Yeah!
  * **14/03/2011:** [[https://es.fbk.eu/events/ssv2011|SSV 2011]] will be co-located with the [[http://itp2011.cs.ru.nl/ITP2011/Home.html|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 [[http://www.cs.aau.dk/~kgl/|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 [[https://es.fbk.eu/events/ssv2011|6th International Workshop on Systems Software Verification]] (SSV 2011).
  * **09/02/2011:** My paper {{:bib:bk11b.pdf|Approximate Quantifier Elimination for Propositional Boolean Formulae}} co-authored with [[http://www.cs.kent.ac.uk/people/staff/amk/|Andy King]] was accepted for [[http://lars-lab.jpl.nasa.gov/nfm2011/|NFM'11]].
  * **07/12/2010:** My paper {{:bib:bk11.pdf|Transfer Function Synthesis without Quantifier Elimination}} co-authored with [[http://www.cs.kent.ac.uk/people/staff/amk/|Andy King]] was accepted for [[http://software.imdea.org/~gbarthe/esop11/|ESOP'11]].
  * **28/10/2010:** Together with [[http://ti.tuwien.ac.at/ecs/people/treinbacher|Thomas Reinbacher]], [[http://embsys.technikum-wien.at/staff/horauer/index.php|Martin Horauer]], [[http://ti.tuwien.ac.at/ecs/people/steininger|Andreas Steininger]] and [[:en:lehrstuhl:mitarbeiter:kowalewski|Stefan Kowalewski]], I received a best paper award for our contribution to [[http://www.memics.cz/2010/index.php|MEMICS'10]].
  * **08/06/2010:** My paper {{:bib:bkk10.pdf|Range Analysis of Microcontroller Code using Bit-Level Congruences}} co-authored with [[http://www.cs.kent.ac.uk/people/staff/amk/|Andy King]] and [[:en:lehrstuhl:mitarbeiter:kowalewski|Stefan Kowalewski]] was accepted for [[https://es.fbk.eu/events/fmics2010/index.php|FMICS'10]].
  * **04/05/2010:** My paper {{:bib:bk10.pdf|Automatic Abstraction for Intervals using Boolean Formulae}} co-authored with [[http://www.cs.kent.ac.uk/people/staff/amk/|Andy King]] was accepted for [[http://sas2010.univ-perp.fr/|SAS'10]].
===== Research Interests =====

  * abstract interpretation of bit-vector programs (see [[http://www.embedded.rwth-aachen.de/mc_square|[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 {{:bib:bk10.pdf|my SAS'10 paper}} or {{:bib:bk11.pdf|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 {{:bib:bkk11a.pdf|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 [[https://es.fbk.eu/events/ssv2011/index.php|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 [[http://www.asmeconferences.org/idetc2011/CallForPapersDetail.cfm|IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications (MESA) 2011]] in Washington DC, USA
  * Program committee for the [[http://es.fbk.eu/events/fmics2010/index.php|15th International Workshop on
Formal Methods for Industrial Critical Systems (FMICS 2010)]] in Antwerp, Belgium
  * Local organizer for the [[http://ssv09.embedded.rwth-aachen.de|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 [[:en:lehrstuhl:mitarbeiter:brauer:publications|here]] (including abstracts), and a list of my co-authors can be found [[:en:lehrstuhl:mitarbeiter:brauer:coauthors|here]].

<BIBTEX: file=publikationen style=I11 sort=timestamp filter=brauer>

===== 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
    * [[:en:lehre:wise1011:formale_methoden]] (Lecture)
  * Summer semester 2010
    * [[:lehre:sose10:programmanalyse]] (Seminar)
  * Winter semester 2009/2010
    * [[:en:lehre:wise0910:formale_methoden]] (Lecture)
    * [[:en:lehre:wise0910:vup_seminar]] (Seminar)
  * Summer semester 2009
    * [[http://www-i2.informatik.rwth-aachen.de/i2/?id=279|Applying Formal Verification Methods to Embedded Systems]] (Seminar)
  * Winter semester 2008/2009
    * [[:en:lehre:wise0809:seminar_statische_analyse]] (Seminar)