About
Hans-Dieter A. Hiep is a Ph.D. student at Leiden University, Leiden Institute of Advanced Computer Science (LIACS), and Centrum Wiskunde & Informatica (CWI), Computer Security group, specializing in Formal Methods. In 2018, he finished a Master program in Computer Science joint-degree at the Vrije Universiteit and Universiteit van Amsterdam (VU/UvA), cum laude, specializing in Foundations of Computing and Concurrency (FCC). In 2016, he finished a Bachelor program in Computer Science, cum laude, also at the Vrije Universiteit.
His main interests are: formal methods, higher-order logic and type theory, program correctness, interactive and automated theorem proving, mathematical logic, and separation logic. Other interests are: Java and Java virtual machines, distributed and concurrent algorithms, formal languages and automata, programming languages, cluster and grid computing, operating systems, computer networking, Web technologies, and graphical user interfaces.
Curriculum Vitae
Full name: Hans-Dieter Anton Hiep
Born: 21 March 1991, Hoorn, North-Holland, the Netherlands
Teaching activities
- (Lecturer) Concepts of Programming Languages, Leiden University, 2021, 2022 (see on-line lectures)
- (Lecturer) Program Correctness, Leiden University, 2020, 2021, 2022, 2023 (see on-line lectures)
- (Student project supervision) Interactive Theorem Prover Project 2, LUdev, Leiden University, 2022
- (Student project supervision) Interactive Theorem Prover Project, LUdev, Leiden University, 2021
- (Student project supervision) Distributed Algorithms Visualization Tool, Individual Systems Project, Vrije Universiteit Amsterdam, 2020
- (Teaching assistant) Program Correctness, Leiden University, 2019
- (Student assistant) Concurrency & Multi-threading, Vrije Universiteit Amsterdam, 2017, 2018
- (Student assistant) Equational programming, Vrije Universiteit Amsterdam, 2017
- (Student assistant) Logic & sets, Vrije Universiteit Amsterdam, 2013
- (Student assistant) Logic & modelling, Vrije Universiteit Amsterdam, 2013
Thesis supervision
Master students
- (Collaborator) Olaf Maathuis, Verifying OpenJDK's LinkedList using KeY, Open Universiteit (OU), Heerlen, 2020
Bachelor students
- (Daily supervisor) Daniel Roos, Visualisation of Distributed Algorithms Executions: Improving the DaViz Tool, Vrije Universiteit (VU), Amsterdam, 2022
- (Daily supervisor) Oualid Azzeggarh, A Concurrent Visual Programming Language, Leiden University (LIACS), Leiden, 2023
- (Daily supervisor) Andy Tatman, Formal Specification and Analysis of OpenJDK’s BitSet Class, Leiden University (LIACS), Leiden, 2023
- (Daily supervisor) Zahir Bingen, Verification of Combinational and Sequential Circuits in LEAN3, Leiden University (LIACS), Leiden, 2023
Internships
- (Daily supervisor) Lazlo de Wijs, Betrokkenheid in een flipped classroom: het vergroten van betrokkenheid bij het kijken van asynchrone online hoorcolleges, Hogeschool van Amsterdam (HvA), Amsterdam, 2022
Research projects
- (Principal investigator) Verified Reowolf, funded by NGI ASSURE
We research and develop a mathematical formalism, using the state-of-the-art theorem prover Coq, for the verification of properties of protocols specified in Protocol Description Language (PDL) that identify precisely under what conditions important properties, such as network integrity and service availability, remain to hold or when they break. - (Principal investigator) Reowolf II, funded by NGI POINTER
Reowolf replaces the decades-old BSD-style socket for Internet communication: offering an innovative, programmable and interoperable connector API at the system-level to support the separation of concerns between privacy and performance optimization. - (Principal investigator) Reowolf, funded by NGI ZERO
The Reowolf project aims to provide connectors as a generalization of BSD-sockets for multi-party communication over the Internet.
Publications
Accepted articles (to appear in print):
- Dynamic Separation Logic, Frank de Boer, Hans-Dieter Hiep, Stijn de Gouw (conference: MFPS'23)
- The Logic of Separation Logic: Models and Proofs, Frank de Boer, Hans-Dieter Hiep, Stijn de Gouw (conference: TABLEAUX'23)
- Formal Specification and Analysis of OpenJDK’s BitSet Class, Andy Tatman, Hans-Dieter Hiep, Stijn de Gouw (conference: iFM'23)
Published articles / reports:
- Integrating ADTs in KeY and their application to History-Based Reasoning about Collection, Jinting Bian, Hans-Dieter Hiep, Frank de Boer, Stijn de Gouw (journal: FMSD) (gold open access)
- Footprint Logic for Object-Oriented Components, Frank de Boer, Stijn de Gouw, Hans-Dieter Hiep, Jinting Bian (conference: FACS2022) (green open access)
- Verifying OpenJDK’s LinkedList using KeY (extended paper), Hans-Dieter Hiep, Olaf Maathuis, Jinting Bian, Frank de Boer, Stijn de Gouw (journal: STTT) (gold open access)
- Integrating ADTs in KeY and their application to History-Based Reasoning, Jinting Bian, Hans-Dieter Hiep, Frank de Boer, Stijn de Gouw (conference: FM2021) (green open access)
- Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic, Frank de Boer, Hans-Dieter Hiep (journal: TOPLAS) (gold open access)
- A Tutorial on Verifying LinkedList Using KeY, Hans-Dieter Hiep, Jinting Bian, Frank de Boer, Stijn de Gouw (chapter in Deductive Software Verification: Future Perspectives) (green open access)
- History-Based Specification and Verification of Java Collections in KeY, Hans-Dieter Hiep, Jinting Bian, Frank de Boer, Stijn de Gouw (conference: iFM2020) (green open access)
- History-based specification and verification of Java collections in KeY (keynote), Frank de Boer, Hans-Dieter Hiep (conference: FTfJP2020) (open access)
- Reowolf: Synchronous Multi-party Communication over the Internet, Christopher Esterhuyse; Hans-Dieter Hiep (conference: FACS2019) (green open access)
- Verifying OpenJDK’s LinkedList using KeY, Hans-Dieter Hiep, Olaf Maathuis, Jinting Bian, Frank de Boer, Stijn de Gouw (conference: TACAS2020) (gold open access)
- Reowolf 1.0: Project Documentation, Christopher Esterhuyse, Hans-Dieter Hiep, Technical Report, CWI (open access)
- Axiomatic Characterization of Trace Reachability for Concurrent Objects, Frank de Boer, Hans-Dieter Hiep (conference: iFM2019) (green open access)
See also this ORCiD page for a list of publications.
Unpublished manuscripts:
- TMP: Time Modulation Protocol, Dalia Papuc, Benjamin Lion, Hans-Dieter Hiep (preprint)
- Compositional Linearizations of Transactional Behavior, Kasper Dokter, Benjamin Lion, Hans-Dieter Hiep
- Reowolf: Executable, Compositional, Synchronous Protocol Specifications, Christopher Esterhuyse, Benjamin Lion, Hans-Dieter Hiep, Farhad Arbab (preprint)
Talks / conferences / workshops
2023
- Dynamic Separation Logic, KeY Symposium 2023, Bergen, Norway
- Dynamic Separation Logic, 39th Conference on Mathematical Foundations of Programming Semantics, Bloomington, Indiana, USA
- Separation Logic in the Light of Substitutions, Universiteit Twente, Formal Methods and Tools group, Enschede, Netherlands
- Separation Logic in the Light of Substitutions, Radboud University, Software Science Seminar, Nijmegen, Netherlands
- Separation Logic in the Light of Substitutions, University of Groningen, Fundamental Computing group, Groningen, Netherlands (tweet)
2022
- A Theory of Substitutions for Separation Logic, Leiden Institute of Advanced Computer Science (LIACS), Theory Group, Leiden, Netherlands
- A Theory of Substitutions for Separation Logic, New challenges in programming language semantics, Lorentz Center, Leiden, Netherlands
- Footprint Logic for Object-Oriented Components, 18th International Conference on Formal Aspects of Component Software, virtual
- TMP: Time Modulation Protocol, HotRFC Lightning Talks at IETF-115, London, United Kingdom (slides)
- Logic in Computer Science: A Short Introduction to Program Correctness, Dutch Association for Logic and Philosophy of the Exact Sciences (VvL) and Dutch Research School of Philosophy (OZWS), Utrecht, Netherlands
- Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic, Leiden Institute of Advanced Computer Science (LIACS), Theory Group, Leiden, Netherlands
2021
- Reasoning about call-by-value recursive procedures in Hoare logic, Amsterdam Coordination Group (ACG), Amsterdam, Netherlands
- Reasoning about ADTs in KeY, The KeYnote Series, virtual
- History-based Specification and Verification of Java Collections in KeY (extended talk), University of Twente, Formal Methods and Tools Group, virtual
2020
- History-based Specification and Verification of Java Collections in KeY (invited presentation), Formal Techniques for Java-like Programs (FTfJP), European Conference on Object-Oriented Programming (ECOOP), virtual
- History-based Specification and Verification of Java Collections in KeY, 16th International Conference on integrated Formal Methods (iFM), virtual (back-up video)
- History-based Specification and Verification of Java Collections in KeY, Amsterdam Coordination Group (ACG), Amsterdam, Netherlands
2019
- Verifying OpenJDK's LinkedList using KeY, KeY Symposium 2019, Manigod, France
- Axiomatic Characterization of Trace Reachability for Concurrent Objects, 15th International Conference on integrated Formal Methods (iFM), Bergen, Norway
- Axiomatic Characterization of Trace Reachability for Concurrent Objects (preliminary version), Third International Workshop on the ABS Modeling Language and Tools, Amsterdam, Netherlands
- Verifying OpenJDK's LinkedList using KeY, IPA Fall Days, Wageningen, Netherlands
- Verifying OpenJDK's LinkedList using KeY, University of Twente, Formal Methods and Tools Group, Enschede, Netherlands
- Attended Lean Together 2019, Amsterdam, Netherlands
- Attended TeReSe 2019, Amsterdam, Netherlands
2018
- Short Pitch: Formal Languages versus Formal Protocols Dutch National Symposium Software Engineering (SEN), Amsterdam, Netherlands
- Yet Another Reo Semantics: Reasoning about Speculative Execution, Amsterdam Coordination Group (ACG), Amsterdam, Netherlands
- Partially Commutative Monoids and Computational Content of Classical Logic, Amsterdam Coordination Group (ACG), Amsterdam, Netherlands
- Participated in 1st International HacKeYthon 2018, Karlsruhe, Germany
2017
- Attended 9th International School on Rewriting (ISR2017), Eindhoven, Netherlands
Professional committees / activities
- Co-chair Education Committee Bachelor Computer Science (Leiden University 2022–2024)
- Artifact Evaluation Committee (ICFP 2023)
- Artifact Evaluation Committee (POPL 2023)
- Artifact Evaluation Committee (TACAS 2021)
- Organizing Committee (SEFM 2020)
- Website Taskforce (CONCUR 2019)
Professional memberships
- De Nederlandse Vereniging voor Logica & Wijsbegeerte der Exacte Wetenschappen (VvL)
- VEReniging Software Engineering Nederland (VERSEN)
- ACademic Cyber Security Society (ACCSS)
- Association for Computing Machinery (ACM)
- The Proof Society
- Stichting Tegen Hackbare Verkiezingen
Media
- Google beloont Nederlandse ontdekkers van gevaarlijke Java-bug, AGconnect, July 13th, 2023
- Google award for discovering bug in Java library, CWI, July 6th, 2023
Employment / professional experience
November 2020 — present
Ph.D. student, Leiden University (Leiden), Leiden Institute of Advanced Computer Science (LIACS), Theory group
November 2018 — October 2018
Ph.D. student, Centrum Wiskunde & Informatica (Amsterdam), Computer Security group
November 2017 — October 2018
Internship, Centrum Wiskunde & Informatica (Amsterdam), Formal Methods group
2017
Internship, Stichting BEMA, Amsterdam
IT consultant, Custommate B.V., Werkendam
2016—2017
Programmer, Inktweb B.V., Alkmaar
2016
IT consultant, Total Medical Solutions B.V., Dordrecht
2015—2018
IT recruiter, Gong Reflections B.V., Amsterdam
Collaborator, HyperReuts, Amstelveen
2014
Programmer, Social Shop B.V., Amsterdam
2013—2015
Co-founder, AEXIZ, Hilversum
2013
Collaborator, WEEVR, Amsterdam
2012
Programmer, Social Shop B.V., Amsterdam
2011—2012
Co-founder, J.P.H. Media, Alkmaar
2010
Programmer, Cillix B.V., Leiden
2008—2009
Programmer, Admicom, Hoorn
Education
November 2018 — present
Doctor of Philosophy (PhD) degree in Computer Science, Leiden University, Factulty of Science, Leiden Institute of Advanced Computer Science (LIACS)
On-going
September 2016 — October 2018
Joint UvA-VU Master of Science (MSc) degree in Computer Science, University of Amsterdam (UvA) and Vrije Universiteit Amsterdam (VU), Faculty of Science, Department of Computer Science
Track: Foundations of Computing and Concurrency
Thesis: A Reo Semantics for Reasoning about Speculative Execution
Thesis supervisors: dr. Jasmin Blanchette, prof.dr. Farhad Arbab
Graduated: cum laude
September 2012 — August 2016
Bachelor of Science (BSc) degree in Computer Science, Vrije Universiteit Amsterdam (VU), Faculty of Science, Department of Computer Science
Minor: Deep Programming
Thesis: Alternative Connectives for Classical Propositional Logic
Thesis supervisors: dr. Femke van Raamsdonk, dr. Clemens Grabmayer
Graduated: cum laude
September 2011 — August 2012
Bachelor Econometrics and Operations Research, University of Amsterdam (UvA), Faculty of Economics and Business, Amsterdam School of Economics
Not graduated
September 2010 — August 2011
Double bachelor Computer Science & Mathematics, Leiden University, Factulty of Science, Leiden Institute of Advanced Computer Science (LIACS)
Not graduated
2003—2010
Voorbereidend wetenschappelijk onderwijs (VWO), Rooms-Katholieke Scholengemeenschap Tabor, Werenfridus, Hoorn
Extracurricular
2018—2022 Secretary of the Board, VU-koor, Amsterdam
2017—2018 Advice committee, VU-koor, Amsterdam
2010—2011 Yearbook committee, De Leidsche Flesch, Leiden