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

2016
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]
2015
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]
2014
Refinement types for TLA+
Stephan Merz and H.V.
6th NASA Formal Methods Symposium (NFM 2014)
© Springer-Verlag, LNCS 8430, pp 143-157 [pdf]
2012
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]
2011
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]
2010
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: