Institut für Rechnerarchitektur
und Parallelrechner
Dr. Dirk Leinenbach
Universität des Saarlandes   Gebäude E1 3
FR 6.2 Informatik   Raum 4.06.3 (Geb.E1.1)
Postfach 151150   Tel: +49 (0)681 302-57379
D-66041 Saarbrücken   Fax: +49 (0)681 302-4290
Germany   eMail: dirkl@cs.uni-saarland.de
 
 
Lebenslauf
1978 Geboren in Illingen
1997 Abitur am Geschw. Scholl Gymnasium in Lebach
1997 - 1998 Zivildienst
1998 - 2002 Informatikstudium an der Universität des Saarlandes
2002 - 2005 Stipendium des Graduiertenkollegs "Leistungsgarantien für Rechnersysteme"
2002 Informatik Diplom
2002 - 2008 Promotion an der Universität des Saarlandes
2003 Günter Hotz Preis
2005 - 2007 Modulkoordinator im Management Team des BMBF Projekts Verisoft
2007 Senior Consultant am DFKI; Mitglied des Management-Teams des BMBF Projekts Verisoft XT
 
Forschungsinteressen
Formale Verifikation
Embedded Systems
Hardwareimplementierung und Verifikation
 
Private Homepage
http://www-wjp.cs.uni-sb.de/leute/individuum.php?person=49
 
Publikationen
Alkassar, E. and Hillebrand, M. A. and Leinenbach, D. C. and Schirmer, N. W. and Starostin, A. and Tsyban, A.   EE BibTeX
Balancing the Load: Leveraging Semantics Stack for Systems Verification.
In Klein, Gerwin and Huuck, Ralf and Schlich, Bastian, editors, Journal of Automated Reasoning: Special Issue on Operating Systems Verification,
pages 389-454, Springer, 2009.
ISBN 0168-7433
 
Hillebrand, M. and Leinenbach, D.   EE BibTeX
Formal Verification of a Reader-Writer Lock Implementation in C.
In 4th International Workshop on Systems Software Verification (SSV09),
volume 254 of Electronic Notes in Theoretical Computer Science, pages 123-141, Elsevier Science B. V., 2009.
 
Cohen, E. and Dahlweid, M. and Hillebrand, M. and Leinenbach, D. and Moskal, M. and Santen, T. and Schulte, W. and Tobies, S.   EE BibTeX
VCC: A Practical System for Verifying Concurrent C.
In Stefan Berghofer and Tobias Nipkow and Christian Urban and Markus Wenzel, editors, Proceedings of the 22nd International Conference on Theorem proving in Higher-Order Logics (TPHOLs 2009),
Munich, Germany
volume 5674 of Lecture Notes in Computer Science, pages 23--42, Springer, 2009.
 
Leinenbach, D. and Santen, T.   EE BibTeX
Verifying the Microsoft Hyper-V Hypervisor with VCC.
In 16th International Symposium on Formal Methods (FM 2009),
Eindhoven, the Netherlands
volume 5850 of Lecture Notes in Computer Science, pages 806-809, Springer, 2009.
Note: Invited paper.
 
Cohen, E. and Alkassar, E. and Boyarinov, V. and Dahlweid, M. and Degenbaev, U. and Hillebrand, M. and Langenstein, B. and Leinenbach, D. and Moskal, M. and Obua, S. and Paul, W. and Pentchev, H. and Petrova, E. and Santen, T. and Schirmer, N. and Schmaltz, S. and Schulte, W. and Shadrin, A. and Tobies, S. and Tsyban, A. and Tverdyshev, S. EE BibTeX
Invariants, Modularity, and Rights.
In Amir Pnueli and Irina Virbitskaite and Andrei Voronkov, editors, Perspectives of Systems Informatics (PSI 2009),
Novosibirsk, Russia
volume 5947 of Lecture Notes in Computer Science, pages 43--55, Springer, 2009.
 
Leinenbach, D. and Petrova, E.   EE BibTeX
Pervasive Compiler Verification -- From Verified Programs to Verified Systems.
In 3rd intl Workshop on Systems Software Verification (SSV08).,
volume 217C of Electronic Notes in Theoretical Computer Science, pages 23-40, Elsevier Science B. V., 2008.
 
Alkassar, Eyad and Hillebrand, Mark A. and Leinenbach, Dirk and Schirmer, Norbert W. and Starostin, Artem EE BibTeX
The Verisoft Approach to Systems Verification.
In Natarajan Shankar and Jim Woodcock, editors, 2nd IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08),
volume 5295 of LNCS, pages 209--224, Springer, 2008.
 
Leinenbach, Dirk   BibTeX
Compiler Verification in the Context of Pervasive System Verification.
2008.
Dissertation, Saarland University, Saarbrücken, 2008
 
Beyer, S. and Jacobi, C. and Kröning, D. and Leinenbach, D. and Paul, W.J.   EE BibTeX
Putting it all together - Formal Verification of the VAMP.
In STTT Journal, Special Issue on Recent Advances in Hardware Verification,
Springer, 2006.
 
Gargano, M. and Hillebrand, M. and Leinenbach, D. and Paul, W.   EE BibTeX
On the Correctness of Operating System Kernels.
In Hurd, J. and Melham, T., editors, Theorem Proving in High Order Logics (TPHOLs) 2005,
Oxford, U.K.
LNCS, Springer, 2005.
 
Leinenbach, D. and Paul, W. and Petrova, E. EE BibTeX
Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctness.
In 3rd International Conference on Software Engineering and Formal Methods (SEFM 2005),
Koblenz, Germany
2005.
Note: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.
 
Beyer, S. and Böhm, P. and Gerke, M. and Hillebrand, M. and In der Rieden, T. and Knapp, S. and Leinenbach, D. and Paul, W.J.   EE BibTeX
Towards the Formal Verification of Lower System Layers in Automotive Systems.
In 23nd IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD 2005), 2-5 October 2005, San Jose, CA, USA, Proceedings,
pages 317-324, IEEE, 2005.
ISBN 0-7695-2451-6
 
In der Rieden, T., and Leinenbach, D., and W. J. Paul   EE BibTeX
Towards the Pervasive Verification of Automotive Systems.
In Dominique Borrione, and Wolfgang Paul, editors, Correct Hardware Design and Verification Methods (CHARME 2005),
volume 3725 of Lecture Notes in Computer Science, pages 3-4, Springer, 2005.
ISBN 3-540-29105-9
 
Beyer, S. and Jacobi, C. and Kröning, D. and Leinenbach, D. and Paul, W.J.   EE BibTeX
Instantiating uninterpreted functional units and memory system: functional verification of the VAMP.
In Geist, D. and Tronci, E., editors, CHARME 2003,
volume 2860 of LNCS, pages 51-65, Springer, 2003.
 
Berg, C. and Beyer, S. and Jacobi, C. and Kröning, D. and Leinenbach, D.   BibTeX
Formal Verification of the VAMP Microprocessor (Project Status).
In Charatonik, Witold and Ganzinger, Harald, editors, Symposium on the Effectiveness of Logic in Computer Science (ELICS02),
pages 31-36, Max-Planck-Institut für Informatik, 2002.
 
Leinenbach, Dirk   BibTeX
Implementierung eines maschinell verifizierten Prozessors.
2002.
Diplomarbeit, Universität des Saarlandes, 2002
 
Beyer, S. and Jacobi, C. and Kroening, D. and Leinenbach, D.   BibTeX
Correct Hardware by Synthesis from PVS.
2002.
unpublished, available at http://www-wjp.cs.uni-sb.de/publikationen/BJKL02.pdf