Hans-Jörg Schurr

Introduction

I am a computer science postdoc at the University of Iowa, where I study SMT solving and work on the solver cvc5. My main research interest is making SMT solver more useful by using expressive type systems. Currently, I am focusing on SMT proof certificates. These certificates must be easy to produce, and easy to check. To solve both goals, we use logical frameworks.

Concretely, we are currently building the Eunoia language that combines ideas from the LFSC framework with the familiar syntax of the Alethe format.

SMT research is driven by solver development and empirical evaluations. I am a developer of cvc5, and the lead developer veriT. I also co-maintain the SMT-LIB benchmark library, and participated in the SMT competition.

My PhD at the Inria Centre at Université de Lorraine was supervised by Pascal Fontaine, Jasmin Blanchette, and Stephan Merz. I worked on the integration of veriT into Isabelle/HOL. This led to the specification of the universal proof format Alethe. I also studied quantifier instantiation and strategy scheduling.

Beyond research, I am passionate about teaching. I taught applied computer science at Polytech Nancy (in French), and undergraduate classes at the University of Iowa.

Content

EMail Me Publications Artifacts Talks Service Teaching Contact

Publications

Color code: Conference Refereed workshop Thesis Informal publication

The arrow (↑) denotes that the authors are in alphabetic order, (↓) denotes reverse alphabetic order.

The Alethe Proof Format: An Evolving Specification and Reference
Barbosa, Haniel, Mathias Fleury, Pascal Fontaine, and Hans-Jörg Schurr (↑)
2025. https://verit.gitlabpages.uliege.be/alethe/specification.pdf
PDF
Optimal Strategy Schedules for Everyone
Schurr, Hans-Jörg
In PAAR@IJCAR 2022.
PDF.bibSlides
Stronger SMT Solvers for Proof Assistants: Proofs, Quantifier Simplification, Strategy Schedules
Schurr, Hans-Jörg
2022. PhD thesis, Université de Lorraine
PDF.bibSlidesHAL
Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Schurr, Hans-Jörg, Mathias Fleury, and Martin Desharnais (↓)
In CADE 2021. LNCS
Authors’ PDFOpen Access.bibSlides
Quantifier Simplification by Unification in SMT
Fontaine, Pascal, and Hans-Jörg Schurr (↑)
In FroCoS 2021. LNCS
Authors’ PDFSpringer Link.bibSlides Best Paper by a Junior Researcher
Alethe: Towards a Generic SMT Proof Format
Schurr, Hans-Jörg, Mathias Fleury, Haniel Barbosa, and Pascal Fontaine
In PxTP 2021.
Extended AbstractSlides
Reconstructing VeriT Proofs in Isabelle/HOL
Fleury, Mathias, and Hans-Jörg Schurr
In PxTP 2019. EPTCS
Authors’ PDFOpen Access.bibSlides
Preprocessing in Higher-Order Reasoning: Learning from QBF Solving
Schurr, Hans Jörg
2017. Master’s thesis, TU Wien
PDF
Capability Discovery for Automated Reasoning Systems
Steen, Alexander, Max Wisniewski, Hans-Jörg Schurr, and Christoph Benzmüller
In IWIL@LPAR 2017. Kalpa Publications in ComputingEasyChair
PDF

Artifacts and Software

cvc5 Role: Developer
cvc5 is feature complete SMT solver that is used in research and industry. It has a long track record of winning at most categories of the SMT competition. As a developer of on the cvc5 team, I contribute to both cvc5 itself and related tools, such as the Ethos proof checker. I was responsible for preparing competition version of cvc5 in 2023 and 2024.
Webpage Github
veriT Role: Lead Developer
veriT is a lightweight SMT solver, with a focus on excellent proofs and short latency. It was the main platform of my PhD work, which led to the integration of veriT with Isabelle/HOL. Currently, veriT receives improvements to proof output and bugfixes.
Webpage
SMT-LIB Benchmarks Role: Co-Maintainer
The SMT-LIB benchmark library is a library of over 400 000 SMT benchmarks. It is used for research and by the SMT competition. The library is part of the larger SMT-LIB project.
Webpage Benchmark Submission Zenodo
schedgen Role: Lead Developer
Schedgen is a tool to generate and analyze strategy schedules for SMT solvers. It uses linear programming and empirical measurements to find optimal strategy schedules that use a set of predefined solving strategies.
Repository PDF

Talks

This section lists most of my recent talks.

Service

2025

Program Committee: SMT

Artifact Evaluation Committee: ATVA

Reviews: TACAS

2024

Program Committee: SBMF

Artifact Evaluation Committee: ICFP ATVA TACAS

Reviews: Sci. Comput. Program. J. Autom. Reason.

2023

Program Committee: SMT

Reviews: FroCoS

2022

Artifact Evaluation Committee: TACAS

Reviews: TACAS SMT Int. J. Softw. Tools Technol. Transf.

2021

Reviews: CADE CAV ICALP KI

Teaching

at The University of Iowa

at Polytech Nancy (in French 🇫🇷)

at FU Berlin

Contact