# Antti Valmari, Professor

Visiting 67°00'00" N 24°00'00" E

I have been a Professor with University of Jyväskylä, Faculty of Information Technology since 2018-01-01. Before that I was a professor with Tampere University of Technology for 25 years.

I apply logic and other branches of discrete mathematics to construct reliable efficient software. So I am somewhere between a practical programmer and a theoretical computer scientist.

## Contact information

• email:
• phone: +358 40 8053362
• address: PO Box 35 (Ag C416.2), FI-40014 University of Jyväskylä, FINLAND
• office: Ag C416.2

## My research

has concentrated on verification algorithms, methods and tools for reactive and concurrent systems. In that field, this is worth mentioning, and also this made me very happy. I also found a link to this, but there are two others I failed to find links to (ACSD 1998, Petri Nets 2012). This is in an entirely different area, and obviously not so much mine.

That line of research has led me to process-algebraic semantic models and to verification-motivated work in data structures and algorithms. If you fancy finite automata, please have a look at this DFA minimizer C++ program, this open access publication, and this publication. The latter has been commented very nicely here.

A much more complicated program for Markov chain lumping and Markov decision process minimization, based on Valmari & Franceschinis: Simple O(m log n) time Markov chain lumping, is here.

Recently I have spent lots of effort in developing computer-aided mathematics and theoretical computer science education. The tool I have been developing is called MathCheck. Unfortunately I have not written sufficient introduction in English, but this and this page introduce two logic modes implemented in 2020.

I have also occasionally studied other problems. I have investigated asymptotic properties of the classic halting problem. This work arose as a spin-off from attempts to explain undecidability to students who have difficulties in accepting the standard undecidability proof. I have also adapted the proof of the classic Shannon memory usage lower bound to a data structure situation where the standard proof does not work.

The membership I am most proud of is this.

## I teach

In the past I have taught several additional topics, including: data structures and algorithms, principles of programming languages, object-oriented programming, introductory theoretical computer science, verification of (sequential) programs, concurrency theory, model checking, and Petri nets.

Petri net 2009 bag in Finnish Lapland
(click for full-size picture)

## My tenure track

A photo of my tenure track
(click for full-size picture)

Latest update 2020-08-21