### About

I'm currently a Postdoc Associate at the Department of Computer Science at Yale University. As a member of Zhong Shao's group, and as part of the DeepSpec project, I'm working on the verification of the CertiKOS operating system.

In December 2014 I defended my Ph.D. thesis entitled *Proof automation
and type synthesis for set theory in the context of TLA ^{+}*, under the supervision of
Stephan Merz.
During this time, I was a member of the VeriDis team at
INRIA Nancy and
Max-Planck-Institute für Informatics, and
of the Tools and Methodologies for Formal Specifications and Proofs
project at the Microsoft-INRIA Joint Lab.

TLA^{+} is a specification language designed to verify concurrent and distributed algorithms.
The first part of my thesis describes the integration of automated first-order provers and SMT solvers
into the TLA^{+} Proof System.
Because TLA^{+}'s underlying logic is based on untyped set theory, only one universal sort is used
to encode TLA^{+} (including arithmetic) into the unsorted and many-sorted logic of automated provers.
In the second part I develop a type system based on refinement types for TLA^{+},
together with a type synthesis algorithm, that are used to improve the encoding and, thus, the user's proof effort.

### Research interests

- Automated and interactive theorem proving
- Logical foundations in Computer Science
- Formal Methods in Software Engineering
- Verification of distributed systems
- Programming languages for certified software

### Publications and presented works

- Encoding TLA
^{+}into many-sorted first-order logic *Stephan Merz and H.V.*- Fifth International Conference on ASM, Alloy, B, TLA, VDM, Z (ABZ 2016).
- © Springer-Verlag, LNCS 9675, pp 54-69 [pdf]

- Encoding TLA
^{+}set theory into many-sorted first-order logic *Stephan Merz and H.V.*- 2nd International Workshop about Sets and Tools (SETS 2015) [pdf]

- Refinement types for TLA
^{+} *Stephan Merz and H.V.*- 6th NASA Formal Methods Symposium (NFM 2014)
- © Springer-Verlag, LNCS 8430, pp 143-157 [pdf]

- Harnessing SMT solvers for TLA
^{+}proofs *Stephan Merz and H.V.*- 12th Intl. Workshop on Automated Verification of Critical Systems (AVoCS 2012)
- © Electronic Communication of the European Association of Software Science and Technology, ECEASST Vol. 53 [pdf]
- TLA
^{+}proofs *Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts and H.V.*- 18th Intl. Symposium on Formal Methods (FM 2012)
- © Springer-Verlag, LNCS 7436, pp. 147-154
- [pdf|extended version|TLA+ module]
- Automatic verification of TLA
^{+}proof obligations with SMT solvers *Stephan Merz and H.V.*- 18th Intl. Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18)
- © Springer-Verlag, LNCS 7180, pp. 289-303 [pdf|slides]

- Towards certification of TLA
^{+}proof obligations with SMT solvers *Stephan Merz and H.V.*- First Workshop on Proof eXchange for Theorem Proving (PxTP, at CADE23) [pdf]

- Formalization of TLA
^{+}arithmetic in the Isabelle proof assistant - (Master Thesis). Director: Stephan Merz.

### Teaching

From 2011 to 2013, I taught at Telecom Nancy, Université de Lorraine, France, as a DCCE (Doctorant Contractuel Chargé d'Enseignement) the following courses:

- Algorithmique des Systèmes Parallèles et Distribués (TD, 2A)
- Modèles et Algorithmes (TD, 2A)
- Techniques et Outils de Programmation (TP, 1A)
- Structures des Données (TP, 1A)