I am a research fellow in the Laboratory for Foundations of Computer Science at Edinburgh.
I am interested in logic for computer science and work mostly on the verification of infinite processes. My current focus is on extensions of vector addition systems / Petri nets, for example with data, pushdown stack, alternation or branching.
Keywords: automata and formal languages, counter systems, pushdown automata, concurrency, algorithmic game theory, wellstructured transition systems, model checking, equivalence checking, bisimulation, decision procedures.
Selected Publications
A full list ist available here and on dblp .

Reachability in TwoDimensional Unary Vector Addition Systems with States is NLComplete
Matthias Englert,
Ranko Lazić,
LICS2016 arxiv pdf slides

A PolynomialTime Algorithm for Reachability in Branching VASS in Dimension One
Stefan Göller,
Christoph Haase,
Ranko Lazić,
ICALP2016 arxiv pdf

BranchingTime Model Checking GapOrder Constraint Systems
Richard Mayr,
Fundamenta Informaticae arxiv bib pdf slides

Simulation Problems Over OneCounter Nets
Piotr Hofman,
Sławomir Lasota,
Richard Mayr,
LMCS arxiv pdf

On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension
Jérôme Leroux,
Grégoire Sutre,
ICALP2015 arxiv bib pdf slides

Trace Inclusion for OneCounter Nets Revisited
Piotr Hofman,
RP2014 arxiv bib pdf slides

InfinteState Energy Games
Parosh Aziz Abdulla,
Mohamed Faouzi Atig,
Piotr Hofman,
Richard Mayr,
K.Narayan Kumar,
LICS2014 arxiv bib pdf
Drafts

MDPs with EnergyParity Objectives
Richard Mayr,
Sven Schewe,
, Dominik Wojtczak
arxiv pdf

Linear Combinations of Unordered Data Vectors
Piotr Hofman,
Jérôme Leroux,
arxiv pdf
Recent Talks

Reachability in TwoDimensional Unary Vector Addition Systems with States is NLComplete
Thu 08 September 2016
@HIGHLIGHTS 2016, Brussels, Belgium
slides

The Reachability Problem for TwoDimensional Vector Addition Systems with States
Wed 09 March 2016
@Theory group seminar, Queen Mary London, UK
slides

The Reachability Problem for TwoDimensional Vector Addition Systems with States
Tue 08 March 2016
@DIMAP seminar, Warwick, UK
slides

Contextfree Controlled Vector Addition Systems
Thu 17 September 2015
@HIGHLIGHTS 2015, Prague, Czech Republic
slides

Monotonicity for OneCounter Systems: What gives?
Thu 17 April 2014
@LaBRI, Bordeaux, France
slides

Inclusion Problems for OneCounter Systems
Thu 14 November 2013
@LaBRI, Bordeaux, France
slides

Hack your inbox: building alot for notmuch
Tue 22 October 2013
@LFCS LabLunch, Edinburgh, UK
slides
Teaching 2015/2016 at Warwick
Short Bio
I spend a year each at the University of Warwick (2015) and LaBRI in Bordeaux (2014), where I had the pleasure of working with Ranko Lazić, Jérôme Leroux and Grégoire Sutre on extended vector addition systems. I did my PhD at LFCS, the University of Edinburgh, supervised by Colin Stirling and Richard Mayr. Before that, I studied informatics and worked as a teaching assistant at the universities of Hamburg and Munich and received a diploma (Dipl. Inf.) from the University of Hamburg.
Misc
I enjoy foosball, good whisky and am overly passionate about free software. In my spare time I develop alot, a terminal MUA for the notmuch mail indexer. I also wrote LaTeX beamer themes designed after the websites of the Universities of Edinburgh and Warwick, which I used for some of my talks.
I have a haindex of 80.
Fun & useful stuff found on the web
 researchinprogress
 shitmyreviewerssay
 Don Knuth on mathematical writing (pdf)
 Ten Simple Rules for Better Figures
 scihub: last resort against evil paywalls
 Filippo Bonchi and Damien Pous: Hacking Nondeterminism with Induction and Coinduction (video)
 This ingeniously named garage close to Coventry