# Biography

I am an Associate Professor based in the Automated Verification Group at the Department of Computer Science at the University of Oxford and a Fellow of St Catherine’s College. The goal of my research is to develop rigorous mathematical methods, algorithms and tools that make hard- and software systems more reliable by automatically discovering bugs or proving their absence. I was awarded an ERC Starting Grant to investigate decision procedures for arithmetic theories in 2019.

I hold a D.Phil. (Ph.D.) degree from the University of Oxford and received an EPSRC doctoral prize for the accomplishments during my doctoral studies. Prior to my current appointment, I have worked at University College London, ENS Paris-Saclay and Microsoft Research Cambridge.

### Interests

• Algorithmic Verification
• Automated Reasoning
• Automata Theory
• Logic in Computer Science

### Education

• DPhil (PhD) in Computer Science, 2012

University of Oxford, UK

• Diplom-Informatiker (BSc/MSc in Computer Science), 2007

Technische Universität Dresden, Germany

• Visiting student, 2005-06

University of Bristol, UK

# Team

### Former members

• Jakub Różycki (2020, internship student)
• Andrei Draghici (2020, internship student)
• Georgina Bumpus (2019, internship student)
• Paul-Ioan Stoienescu (2019, internship student)
• Jonathan Tanner (2019, internship student)
• Florent Guépin (2018, internship student)
• Simon Halfon (2014, internship student)

# Projects

ARiAT is an ERC-funded project investigating decision procedures for arithmetic theories.

# Recent publications

(2021). Directed Reachability for Infinite-State Systems. Tools and Algorithms for the Construction and Analysis of Systems, TACAS.

(2021). On deciding linear arithmetic constraints over $p$-adic integers for all primes. Mathematical Foundations of Computer Science, MFCS.

(2021). On the Expressiveness of Büchi Arithmetic. Foundations of Software Science and Computation Structures, FOSSACS.

# Students

## Prospective PhD students

If you are interested in doing research on topics related to my research interests, please do get in touch for informal enquiries! I can offer a broad variety of topics to work on, ranging from fundamental problems in the theory of computation to engineering cutting-edge tools. You are of course welcome and encouraged to propose your own topics.

For more information on applying for a D.Phil. (that’s Oxford terminology for a Ph.D.), take a look at the Department’s webpage.

## Previously supervised students

### Research internships

• Jakub Różycki: On the Expressiveness of Büchi Arithmetic (2020, the results appeared in FoSSaCS)
• Andrei Draghici: Neuro-guided SAT solving (2020)
• Georgina Bumpus, Paul-Ioan Stoienescu, Jonathan Tanner: On the Size of Finite Rational Matrix Semigroups (2019, co-supervised with S. Kiefer, the results appeared in ICALP)
• Florent Guépin: On the Existential Theories of Büchi Arithmetic and Linear p-adic Fields (2018, co-supervised with J. Worrell, the results appeared in LICS)
• Simon Halfon: Non Primitive Recursive Complexity Classes (2014, co-supervised with S. Schmitz and Ph. Schnoebelen, some results appeared in RP and TCS)

### Thesis supervision

• Alex Fung: On the Expressivene Completeness of Büchi Arithmetic (2020, 4th year MEng Mathematical Computation project)
• Andrei Draghici: Boolean Operations on Semi-Linear Sets (2019-20, 3rd year Computer Science project)
• Serban Slincu: Decision Procedures for Linear Arithmetic Theories (2019-20, 3rd year Computer Science project)
• Bozhidar Vasilev: Approaching Intractable Problems with SAT and SMT (2019-20, 3rd year Computer Science project)
• Axel Ronquist: A Lower Bound on the Complexity of Real Addition Without Order (2018-19, 4th year Computer Science and Philosophy project)
• Michał Kreft: On the Complexity of Deciding Whether Ordering is Necessary in a Presburger Formula (2017-18, 4th year Mathematics and Computer Science project)
• Ciprian Stirbu: Parallel Algorithms for Computing Hilbert Bases (2017-18, 3rd year Computer Science project)

# Contact

• {firstname}.{lastname}@cs.ox.ac.uk
• Departement of Computer Science, University of Oxford, Parks Rd, Oxford, OX1 3QD, United Kingdom
• Wolfson Building, 4th floor, Room 407