Institut für Rechnerarchitektur und Parallelrechner

Dr. Mark A. Hillebrand

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: mah@cs.uni-saarland.de

Lebenslauf

1976		Geboren in Neuss
1995		Abitur am Geschwister-Scholl-Gymnasium in Düsseldorf
1996 - 2000		Studium der Informatik an der Universität des Saarlandes
2000		Diplom in Informatik
2000 - 2002		Im Rahmen der Promotion Mitarbeit bei IBM Entwicklung & Forschung GmbH, Böblingen.
2000 - 2005		Promotion an der Universität des Saarlandes

Forschungsinteressen

Formale Verifikation von Low-Level Betriebssystemsoftware

Formale Verifikation von Hardware

Hardware Design

Private Homepage

http://www-wjp.cs.uni-sb.de/leute/private_homepages/mah/Homepage/Index.html

Publikationen

Klebanov, V and Müller, P. and Shankar, N. and Leavens, G. and Wüstholz, V. and Alkassar, E. and Arthan, R. and Bronish, D. and Chapman, R. and Cohen, E. and Hillebrand, M. and Jacobs, B and Leino, R. and Monahan, R. and Piessens, F. and Polikarpova, N. and Ridge, T. and Smans, J. and Tobies, S. and Tuerk, T. and Ulbrich, M. and Wei, B.		BibTeX
The 1st Verified Software Competition: Experience Report.
In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods (FM 2011),
LNCS, 2011.
Note: Best Paper Award

Alkassar, E. and Hillebrand, M. and Paul, W. and Petrova, E.	EE	BibTeX
Automated Verification of a Small Hypervisor.
In Third International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'10),
Edinburgh, UK
volume 6217 of LNCS, pages 40-54, Springer, 2010.

Alkassar, E. and Cohen, E. and Hillebrand, M. and Kovalev, M. and Paul, W.		BibTeX
Verifying Shadow Page Table Algorithms.
In Formal Methods in Computer Aided Design (FMCAD) 2010,
Lugano, Switzerland
pages 267-270, IEEE, 2010.

Alkassar, E. and Cohen, E. and Hillebrand, M. and Pentchev, H.		BibTeX
Modular Specification and Verification of Interprocess Communication.
In Formal Methods in Computer Aided Design (FMCAD) 2010,
IEEE, 2010.
Note: to appear

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 Tverdyshev, S.	EE	BibTeX
Formal Verification of Gate-Level Computer Systems.
In A. Morozov, K. Wagner, A. Rybalchenko, and A. Frid., editors, 4th International Computer Science Symposium in Russia,
volume 5675 of LNCS, pages 322-333, Springer, 2009.

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.

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.

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.

Alkassar, Eyad and Hillebrand, Mark A.	EE	BibTeX
Formal Functional Verification of Device Drivers.
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 225--239, Springer, 2008.

Alkassar, E. and Hillebrand, M. and Knapp, S. and Rusev, R. and Tverdyshev, S.	EE	BibTeX
Formal Device and Programming Model for a Serial Interface.
In B. Beckert, editors, Proceedings, 4th International Verification Workshop (VERIFY), Bremen, Germany,
pages 4--20, CEUR-WS Workshop Proceedings, 2007.

Hillebrand, M. A. and Paul, W. J.	EE	BibTeX
On the Architecture of System Verification Environments.
In Karen Yorav, editors, Haifa Verification Conference 2007, October 23-25, 2007, Haifa, Israel,
volume 4899 of LNCS, pages 153--168, Springer, 2007.

Hillebrand, Mark		BibTeX
Address Spaces and Virtual Memory: Specification, Implementation, and Correctness.

Dissertation, Saarland University, Saarbrücken, 2005.

Dalinger, I. and Hillebrand, M. and Paul, W.	EE	BibTeX
On the Verification of Memory Management Mechanisms.
In Borrione, D. and Paul, W., editors, CHARME 2005,
LNCS, Springer, 2005.

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.

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

Hillebrand, M. and In der Rieden, T. and Paul, W.J.	EE	BibTeX
Dealing with I/O Devices in the Context of Pervasive System Verification.
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 309-316, IEEE, 2005.
ISBN 0-7695-2451-6

Hillebrand, Mark and Schuerger, Thomas and Seidel, Peter-M.	EE	BibTeX
How to Halve Wire Lengths in the Layout of Cyclic Shifters.
In Proceedings of the IEEE International Conference on VLSI Design 2001,
pages 339-344, IEEE Computer Society Press, 2001.

Hillebrand, Mark and Schuerger, Thomas and Seidel, Peter-M.	EE	BibTeX
Reducing Wire Lengths in the Layout of Cyclic Shifters.
In IEICE Transactions, Special Section on VLSI and CAD Algorithms,
pages 2714-2721, 2001.

Hillebrand, Mark A.		BibTeX
Design and Evaluation of a Superscalar RISC Processor.

Diplomarbeit, Saarland University, Saarbrücken, 2000.

Grün, T. and Hillebrand, M.A.	EE	BibTeX
NAS Integer Sort on Multi-threaded Shared Memory Machines.
In Proc. EuroPar 98,
volume 1470 of Lecture Notes in Computer Science, Springer Verlag, 1998.