Thomas Reinbacher

Thomas Reinbacher
BSc MSc Mag.rer.soc.oec. Dr.techn.

Thomas Reinbacher
E-Mail treinbacher@ecs.tuwien.ac.at
my PGP public key
Phone +43 (1) 58801-18203
Fax +43 (1) 58801-18297
Address



Vienna University of Technology

Department of Computer Engineering
Embedded Computing Systems Group
Treitlstrasse 1-3 / 2nd floor

 

News

  • 05-05-2014
    I'll present my thesis at the GI-Dissertationspreis 2013 Kolloquium at Schloss Dagstuhl this week.
  • 10-01-2014
    The paper Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems that I co-authored with Kristin Y. Rozier from NASA Ames Research Center and Johann Schumann from SGT. Inc, NASA Ames Research Center has been accepted to TACAS'14. In this paper, we develop new runtime observers to enable system health management of real-time systems such as air- and spacecraft.
  • 15-10-2013
    The paper Towards Real-time, On-board, Hardware-supported Sensor and Software Health Management for UAS that I co-authored with Johann Schumann from SGT. Inc, NASA Ames Research Center, Kristin Y. Rozier from NASA Ames Research Center, Ole Mengshoel from CMU-SV, Timmy Mbaya from University of Southern Californa, Los Angeles, as well as Corey Ippolito from NASA Ames Research Center has been accepted to PHM'13. In this paper, we develop a new approach to health management of unmanned aerial systems.
  • 30-06-2013
    The paper Template-Based Synthesis of Plan Execution Monitors that I co-authored with César Guzmán Alvarez from Universitat Politècnica de València has been accepted to HAIS'13. In this paper, we exploit the benefits of automatically synthesizing observers that monitor the execution of a plan in a mars rover scenario.
  • 21-06-2013
    I successfully defended my PhD thesis "Analysis of Embedded Real-Time Systems at Runtime".
  • 03-11-2012
    The journal article Runtime Verification of Microcontroller Binary Code (a sequel of our FMICS'11 paper) that I co-authored with Jörg Brauer, Martin Horauer, Andreas Steininger, and Stefan Kowalewski has been accepted to be published in the journal Science of Computer Programming. In this article, we propose a runtime verificaton approach to analyze real-life binary code executed on various embedded targets.
  • 30-07-2012
    The paper Real-Time Runtime Verification on Chip that I co-authored with Matthias Függer and Jörg Brauer has been accepted to RV'12. In this paper, we present an algorithmic framework that allows on-line motioning of past-time MTL specifications into efficient observer hardware blocks, which take advantage of the highly-parallel nature of hardware designs. For the time-bounded Since operator we get arrive at a time complexity that is double logarithmic in the time it is executed at and the given time bounds of the Since operator.
  • 16-07-2012
    From mid July to October 2012 I'm @ NASA Ames Research Center to collaborate with the Robust Software Engineering group.
  • 08-07-2012
    The Paper A Runtime Verification Unit for Microcontrollers that I co-authored with Martin Horauer and Andreas Steininger, has been accepted to S4d'12. In this paper, we show how our runtime verification framework can be deployed as a watchdog unit replacement on microcontrollers.
  • 24-04-2012
    The paper Parallel Runtime Verification of Temporal Properties for Embedded Software that I co-authored with Johannes Geist, Patrick Moosbrugger, Martin Horauer and Andreas Steininger, has been accepted to MESA'12. In this paper, we extend our runtime verification framework to a highly parallel setting, that yields a close to linear speedup compared to a single core implementation.
  • 19-01-2012
    I'll be visiting the Embedded Software Laboratory @ RWTH Aachen University from January 8-20 to cooperate on runtime verification of binary code
  • 09-10-2011
    I'll attend the ESWeek in Taipei this week.
  • 19-09-2011
    I'll attend the Runtime Verification Conference in San Francisco this week.
  • 30-08-2011
    We have received the best paper award at FMICS'11 for our paper "Past Time LTL Runtime Verification for Microcontroller Binary Code".
  • 01-08-2011
    Our paper Automated Test-Trace Inspection for Microcontroller Binary Code that I co-authored with Jörg Brauer, Daniel Schachinger, Andreas Steininger and Stefan Kowalewski, has been accepted to RV'11. In this paper, we describe a non-intrusive framework for runtime verification of executable microcontroller code. The framework includes a custom-designed, resource friendly, microcontroller that evaluates ptLTL specification in parallel to program execution.
  • 03-07-2011
    The paper Precise Control Flow Reconstruction Using Boolean Logic that I co-authored with Jörg Brauer, my colleague from RWTH Aachen, has been accepted to EMSOFT'11. In this paper, we combine several techniques such as bit-blasting, Jörg's CAV'11 elimination algorithm and interleaved forward/backward analysis to compute fairly precise approximations of CFGs from binary code.
  • 06-05-2011
    Our workshop paper "Testing Microcontroller Software Simulators" was accepted for WS4C'11.
  • 11-06-2011
    I'll attend the SAT/SMT summer school @MIT in Boston this week.
  • 06-05-2011
    Our paper "Past Time LTL Runtime Verification for Microcontroller Binary Code" was accepted for FMICS'11. In this paper, we show how to perform runtime verification for binary code without code instrumentation.
  • 29-04-2011
    Our paper "Hardware Support for Efficient Testing of Embedded Software" was accepted for MESA'11. The aim of this work is a hardware unit that is (a) easily attachable to an off-the-shelf microcontroller IP-core and (b) allows to validate whether a property violation found by abstract interpretation of binary code also exhibits in a concrete run of the system.
  • 14-07-2011
    I'll be visiting the Embedded Software Laboratory @ RWTH Aachen University from Mid January to March to cooperate on abstract interpretation of microcontroller binary code
  • November-2010
    We've received a best paper award at MEMICS'10 for our paper "Test-Case Generation for Embedded Binary Code Using Abstract Interpretation".
  • 07-07-2010
    From mid July to mid August 2010 I'll be @ RWTH Aachen University to work together with the Embedded Software Laboratory

About me

I was a PhD student at Vienna University of Technology, Department of Computer Engineering, Embedded Computing Systems Group from March 2010 to June 2013.

Before joining the Embedded Computing Systems Group, I was engaged in the FHplus sponsored research project DECS where I worked on model checking and static analysis of binary code for embedded targets. I received both my B.Sc. and M.Sc. degree in electrical engineering / embedded systems from the University of Applied Sciences Technikum Wien, Austria in 2007 and 2009, respectively. During spring term 2007 I did an internship at SIEMENS PSE NanJing, China and in 2009 I studied Chinese Culture and Language at Zhejiang University in HangZhou, China. Later, I was granted a three year FFG FIT-IT doctoral scholarship for the project CevTes and started to work on my thesis under supervision of Prof. Andreas Steininger in April 2010. The research project CevTes (CounterExample Validation and Test-Case Generation Framework for Verifying Embedded Software) is about automated test-case generation based on binary code (formal) analysis with applications for embedded software. CevTes is a joint project of Vienna University of Technology, the University of Applied Sciences Technikum Wien, and the RWTH Aachen University. I held visiting scientist positions at the Embedded Software Laboratory at RWTH Aachen, Germany and at the Robust Software Engineering group at NASA Ames Research Center, CA, USA. I successfully defended my PhD thesis in June 2013.

After three amazing years, I left Vienna University of Technology. Please visit my private website: http://thomasreinbacher.wasner.it for further updates.

My full CV is available here: threinbacher_cv.pdf

Research interests

  • Runtime analysis and formal verification techniques of embedded computing systems with applications in safety critical, high reliability systems as found in the aeronautics, aviation and automotive domain

  • Automated test case generation/execution for embedded software and binary code

Bachelor & Master thesis

We currently have a number of different topics for bachelor and masters theses. If you are interested in working on verification and automated test-case generation for embedded software, please contact either me, Prof. Andreas Steininger, or FH-Prof. Martin Horauer. We offer interesting topics, intensive supervision/mentoring, and free coffee ;)

Publications

Journals

RFB13 T. Reinbacher, M. Fuegger, and J. Brauer Runtime Verification of Embedded Real-Time Systems, Formal Methods in System Design (FMSD), 2013, to appear. [journal]
RBH+12 T. Reinbacher, J. Brauer, M. Horauer, A. Steininger, and S. Kowalewski Runtime Verification of Microcontroller Binary Code, Science of Computer Programming (SCP), 2012, to appear. [journal]
RHS+10 T. Reinbacher, M. Horauer, B. Schlich, J. Brauer, and F. Scheuer, Model checking assembly code of an industrial knitting machine, International Journal of Information Technology, Communications and Convergence (IJITCC), 2010, to appear. [journal]

Reviewed conference papers

RRS14 T.Reinbacher, K. Y. Rozier, and J. Schumann Temporal-Logic Based Runtime Observer Pairs for System Health Mangement of Real-Time Systems, in 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), accepted. [ conference ]
SRR+13 J. Schumann, K. Y. Rozier, T. Reinbacher, O. Mengshoel, T. Mbaya, and C. Ippolito, Towards Real-time, On-board, Hardware-supported Sensor and Software Health Management for UAS, in Proceedings of the Annual Conference of the Prognostics and Health Management Society (PHM'13), New Orleans, USA, accepted. [ conference ]
RGB13 T. Reinbacher and C. Guzman, Template-Based Synthesis of Plan Execution Monitors, in Proceedings of the 8th International Conference on Hybrid Artificial Intelligence Systems (HAIS'13), Salamanca, Spain, accepted. [ conference ]
RNB12 T. Reinbacher, M. Fuegger, and J. Brauer, Real-Time Runtime Verification on chip, in Proceedings of the 3rd International Conference on Runtime Verification (RV'12), September 25 – September 28, 2012, Istanbul, Turkey, accepted. [ conference ]
RHS12 T. Reinbacher, M. Horauer, and A. Steininger, A Runtime Verification Unit for Microcontrolles, in Proceedings of the 4th System, Software, SoC and Silicon Debug Conference (S4D'12), Vienna, Austria, September 19-20, 2012, accepted. [ conference ]
RGM+12 T. Reinbacher, J. Geist, P. Moosbrugger, M. Horauer, and A. Steininger, Parallel runtime verification of temporal properties for embedded software, in Proceedings of the 8th IEEE/ASME International Conference on Mechatronic and Embedded Systems and Applications (MESA'12), Suzhou, China, July 8-10, 2012, pp. 224-231. [ conference ]
RBS+11 T. Reinbacher, J. Brauer, D. Schachinger, A. Steininger, and S. Kowalewski, Automated Test-Trace Inspection for Microcontroller Binary Code, in Proceedings of the 2nd International Conference on Runtime Verification(RV'11), San Francisco, California, US, September 27 - September 30, 2011, pp. 239-244. [ conference ]
RB11 T. Reinbacher and J. Brauer, Precise Control Flow Reconstruction Using Boolean Logic, in Proceedings of the 11th International Conference on Embedded Software(EMSOFT'11), Taipei, Taiwan, October 09-14 2011, accepted. [ conference ]
RGKH11 T. Reinbacher, D.Gueckel, M. Horauer, and S. Kowalewski, Testing Microcontroller Software Simulators, in Proceedings of the Workshop on SLE for CPS at INFORMATIK 2011 (WS4C'11), Berlin, Germany, October 04-07 2011, accepted. [ conference ]
RBH+11 T. Reinbacher, J. Brauer, M. Horauer, A. Steininger, and S. Kowalewski, Past Time LTL Runtime Verification for Microcontroller Binary Code, in Proceedings of the 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'11), Trento, Italy, August 29-30 2011, Best Paper Award. [ conference ]
RSM+11 T. Reinbacher, A. Steininger, T. Mueller, M. Horauer, J. Brauer, and S. Kowalewski, Hardware Support for Efficient Testing of Embedded Software, in Proceedings of the 7th International ASME/IEEE Conference on Mechatronics & Embedded Systems & Applications (MESA'11), Washington, DC, USA, August 28-31 2011, accepted. [ conference ]
RBH+10 T. Reinbacher, J. Brauer, M. Horauer, A. Steininger, and S. Kowalewski, Test-case generation for embedded binary code using abstract interpretation, in Proceedings of the Annual Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10), Mikulov, Czech Republic, October 22- 24 2010, pp. 151-158, Best Paper Award. [ conference ]
RH10 T. Reinbacher and M. Horauer, Formale Verifikation von Embedded Systems Software, in Proceedings of the Microelectronics Conference me10, Vienna, Austria, April 7-8 2010, pp. 289-296, in German. [ conference ]
RHS+09 T. Reinbacher, M. Horauer, B. Schlich, J. Brauer, and F. Scheuer, Model checking assembly code of an industrial knitting machine, in Proceedings of the 4th IEEE International Conference on Embedded and Multimedia Computing (EM-Com 2009), Jeju, Korea, December 10-12 2009, pp. 97-104. [ DOI |conference ]
BSRK09 J. Brauer, B. Schlich, T. Reinbacher, and S. Kowalewski, Stack bounds analysis for microcontroller assembly code, in Proceedings of the 4th Workshop on Embedded Systems Security (WESS 2009), Grenoble, France, October 2009, pp. 1-9. [ DOI | conference ]
RBHS09 T. Reinbacher, J. Brauer, M. Horauer, and B. Schlich, Refining assembly code static analysis for the Intel MCS-51 microcontroller, in Proceedings of the 4th Int'l Symposium on Industrial Embedded Systems (SIES 2009), Lausanne, Switzerland, July 8-10 2009, pp. 161-170. [ DOI |conference ]
RHS09 T. Reinbacher, M. Horauer, and B. Schlich, Using 3-valued memory representation for state space reduction in embedded assembly code model checking, in Proceedings of the 12th IEEE Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2009), Liberec, Czech Republic, April 15-17 2009, pp. 114-119. [ DOI |conference ]
RKHS08b T. Reinbacher, M. Kramer, M. Horauer, and B. Schlich, Motivating model checking for embedded systems software, in Proceedings of the 4th IEEE/ASME Int'l Conf. Mechatronic and Embedded Systems and Applications (MESA 2008), Beijing, China, October 2008, pp. 546-551. [ DOI | conference ]
RKHS08 T. Reinbacher, M. Kramer, M. Horauer, and B. Schlich, Challenges in embedded model checking - a simulator for the [mc]square model checker, in Proceedings of the 3rd Int'l Symposium on Industrial Embedded Systems (SIES 2008), Montpellier, France, 2008, pp. 245-248. [ DOI |conference ]

Master theses

Rei10 T. Reinbacher, Teaching software verification for Higher Technical and Vocational Colleges (HTL) under consideration of educational standards, Master's thesis, Institute of Software Technology and Interactive Systems, Vienna University of Technology, May 2010
Rei09 T. Reinbacher, Model checking and static analysis of MCS-51 assembly code, Master's thesis, Department of Embedded Systems, University of Applied Sciences Technikum Wien, June 2009. [ PDF ]

 

Private

You might have a look at my private website http://thomasreinbacher.wasner.it