Antti Valmari, Professor

Homepage in Finnish behind this link

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

Some recent talks

• Modelling Without a Modelling Language (SPIN 2018)
• Stubborn Sets with Frozen Actions (RP 2017)
• The Logics Taught and Used at High Schools Are Not the Same (RuFiDiM IV)
• More Stubborn Set Methods for Process Algebras (symposium in honour of Bill Roscoe’s 60th birthday)
• The Congruences Below Fair Testing with Initial Stability (ACSD 2016)
• Stubborn Set Intuition Explained (PNSE 2016)
• Stop it, and Be Stubborn! (ACSD 2015)
• A Simple Character String Proof of the “True but Unprovable” Version of Gödel's First Incompleteness Theorem (AFL 2014)
• The Asymptotic Behaviour of the Proportion of Hard Instances of the Halting Problem (SPLST 2013)
• Sizes of Up-to-n Halting Testers (RuFiDiM 2012)
• All Linear-Time Congruences for Familiar Operators (ACSD 2012 and Concur 2012)
• Old And New Algorithms for Minimal Coverability Sets (Petri Nets 2012)
• Does the Shannon Bound Really Apply to Data Structures? (SPLST 2011)

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

• TIEP1020 Diskreetit rakenteet (Discrete Structures), spring 2018–
• TIES3510 Joukko-oppi ja logiikka ohjelmoinnissa (Set theory and Logic in Programming) autumn 2020–
• TIEA241 Automaatit ja kieliopit (Automata and Grammars), autumn 2018–2019

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)

Other info

Curriculum Vitae • Publications • Google Scholar • DBLP

My tenure track

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

Latest update 2020-08-21