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.

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

• 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)