Dr. rer. nat. Dominique Marcel Gückel

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

• German (first language)
• English (fluent)
• French (fluent)
• Latin (degree: Latinum)
• Spanish (basic knowledge)

• 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 PDF.

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

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.

• SS08: Exercises for the lecture Formal Methods for Embedded Systems
• SS09: Proseminar Embedded Systems
• WS09/10: Seminar Verification and Program Analysis
• WS10/11: Exercises for the lecture Formal Methods for Embedded Systems

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

• [mc]square
• DFG Research Training Group 1298 AlgoSyn