====== Dr. rer. nat. Dominique Marcel Gückel ======
~~NOTOC~~
\\
{|
|-
||{{:lehrstuhl:mitarbeiter:gueckel.jpg|}}
||
Research Assistant\\
gueckel[at]embedded[dot]rwth-aachen[dot]de\\
\\
Phone +49 241 80 21168\\
Fax +49 241 80 22150\\
\\
Address: Ahornstr. 55, 52074 Aachen\\
Office: room 2307 (building H)
|}

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

I am a research assistant at the Embedded Software Laboratory of RWTH Aachen since January 2011. Before that, I used to be a scholarship holder in the DFG Research Training Group (Graduiertenkolleg) [[http://www.algosyn.rwth-aachen.de/|AlgoSyn]] since January 2008. I conduct my research at the Embedded Software Laboratory of RWTH Aachen (Chair of Computer Science 11). The intention of my research is to extend the model checking tool [mc]square by synthesis functions.\\


== Languages ==
  * German (first language)
  * English (fluent)
  * French (fluent)
  * Latin (degree: Latinum)
  * Spanish (basic knowledge)

===== Activities =====
  * Leader (lead editor) of the proceedings group for the Proceedings of the Joint Workshop of the German Research Training Groups in Computer Science, Dagstuhl 2010. Printed version available (ISBN 386-130-146-6). Online version of the volume available as [[http://www.algosyn.rwth-aachen.de/GK%20Workshop/Dagstuhl2010.pdf|PDF]].

===== Publications =====

  * Dominique Gückel: Erweiterung des Model-Checkers [mc]square um benutzerdefinierte Umgebungen. Diplomarbeit, RWTH Aachen, 2007.

  * Bastian Schlich, Dominique Gückel, and Stefan Kowalewski. Modeling the Environment of Microcontrollers to Tackle the State-Explosion Problem in Model Checking. In //Proceedings of Symposium Formal Methods for Automation and Safety in Railway and Automotive Systems (FORMS/FORMAT 2008)//, ISBN 978 963 236 138 3. PDF

  * Dominique Gückel. Retargeting a Hardware-Dependent Model Checker by Using Architecture Description Languages. In //Doctoral Symposium on Systems Software Verification (DS SSV 2009) , 4th International Workshop on Systems Software Verification (SSV 09)//, ISSN 0935–3232. [[http://sunsite.informatik.rwth-aachen.de/Publications/AIB/2009/2009-14.pdf|PDF]]

  * Wolfgang Thomas, Kai Bollue, Dominique Gückel, Gustavo Quiros, Michaela Slaats and Michael Ummels. DFG Research Training Group "Algorithmic Synthesis of Reactive and Discrete-Continuous Systems (AlgoSyn)". In //it - Information Technology, Volume 4 /2009//, Oldenbourg, pp. 222-230.

  * Dominique Gückel, Bastian Schlich, Jörg Brauer, and Stefan Kowalewski. Synthesizing Simulators For Model Checking Microcontroller Binary Code. In //Proceedings of 13th IEEE International Symposium on Design & Diagnostics of Electronic Circuits and Systems (DDECS 2010)//, ISBN 978-1-4244-6611-5, pp. 313-316.

  * Dominique Gückel. Synthesis of Hardware Simulators for Use in Model Checking. In //Dagstuhl 2010. Proceedings of the Joint Workshop of the German Research Training Groups in Computer Science//, ISBN 386-130-146-6, p. 76. [[http://www.algosyn.rwth-aachen.de/GK%20Workshop/Dagstuhl2010.pdf|PDF]]

  * Dominique Gückel, Jörg Brauer, and Stefan Kowalewski. A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification. In //Proceedings of 5th IEEE Symposium on Industrial Embedded Systems (SIES 2010)//, ISBN 978-1-4244-5840-0, pp. 118-127.
  * Sebastian Biallas, Jörg Brauer, Dominique Gückel, and Stefan Kowalewski. On-The-Fly Path Reduction. 4th International Workshop on Harnessing Theories for Tool Support in Software (TTSS'10), to appear.
  * Thomas Reinbacher, Dominique Gückel, Martin Horauer, and Stefan Kowalewski. Testing Microcontroller Software Simulators. In //Proceedings of the Workshop on SLE for CPS at INFORMATIK 2011 (WS4C11)//, to appear.
  * Dominique Gückel and Stefan Kowalewski. Automatic Derivation of Abstract Semantics From Instruction Set Descriptions. In //Proceedings of the 6th International Workshop on Systems Software Verification (SSV 2011)//, to appear.


===== Bachelor / Diploma / Master Theses =====

**Ongoing**

   * Florian Caron: State Partitioning for Model Checking Binary Code (Bachelor thesis)

**Finished**

  * Ivica Bogosavljevic: Synthesizing an Instruction Set Simulator for Model Checking Embedded Systems Software (Master thesis)
  * Sebastian Wehlmann: Tool-based implementation of a simulator for Renesas R8C/Tiny microcontrollers for extending the model checker [mc]square (Diploma thesis)

**Open**
    *  Tool-based implementation of a microcontroller simulator
    * Realization of abstraction techniques for supporting nondeterminism in synthetic simulators
    * Extending a simulator synthesis framework by static analyses

More topics are available on request.

===== Teaching =====

  * SS08: Exercises for the lecture [[:en:lehre:sose08:formale_methoden]]
  * SS09: Proseminar [[:en:lehre:sose09:proseminar_eingebettete_systeme]]
  * WS09/10: Seminar [[:en:lehre:wise0910:vup_seminar]]
  * WS10/11: Exercises for the lecture [[:en:lehre:wise1011:formale_methoden]]
 
Besides, I regularly supervise examinations in the lab course //Hardwarenahe Programmierung// (for undergraduate students in the bachelor programme). In the past, I also supervised exams in the lab course //Elektronische Grundlagen für Informatiker// (//foundations of electronics for computer scientists//).

===== Links =====

  * [[http://www-i11.informatik.rwth-aachen.de/mc_square/|[mc]square]]
  * [[http://www.algosyn.rwth-aachen.de/|DFG Research Training Group 1298 AlgoSyn]]