Fairer work schedules and more trustworthy automated systems through automated reasoning

Professor Matti Järvisalo strives to develop increasingly effective algorithmic solution methods to computational problems that require exactness and correctness.

What are your research topics?

I study the automation of logical reasoning and optimisation with computers on both the theoretical and practical levels. My primary goal is to produce effective general algorithmic methods to complex computational problems arising from the real world.

Where and how does the topic of your research have an impact? 

The ability to solve challenging optimisation problems can improve our everyday lives in many ways. The more sensible work schedules we can follow, the faster the courier can deliver packages, or the better routes we have from point A to point B with various means of transport, the more satisfied we are likely to be. In other words, the more effectively we are able to use limited resources, from monetary to natural, in producing various goods and services, the more responsibly we are able to act.

Furthermore, as individuals and as a society, we broadly rely on IT systems in our everyday lives. Often, we only realise this when there are faults in the systems. In particular, faults in safety-critical systems – such as aircraft autopilot systems – can have catastrophic consequences. Proving that IT-systems are guaranteed to work correctly is in such settings of critical importance.

Problems of this nature are so complex that it is usually impossible for humans to identify optimal solutions manually. The increasingly effective algorithmic techniques for automated reasoning developed in my research field make it possible, for example, to develop provably correct hardware and software systems. In addition, they can be used to prove or disprove so-far unresolved mathematical hypotheses.

What is particularly inspiring in your field right now?

The field is developing at a rapid pace and new application settings are continually emerging.

This poses new research challenges, among the latest of which is the development of techniques for verifying the validity of certificates produced by automated means.

In various types of practical problems fair solutions are specifically sought for. For instance, the fair distribution of duties among employees may in cases be more important that to simply minimise costs.

Furthermore, the use of AI techniques as decision-making tools requires the ability to explain to people why the techniques are proposing specific decisions and why those suggestions can be trusted.


Matti Järvisalo is the Professor of Computer Science (algorithms and machine learning) at the Faculty of Science.

Read about the other newly appointed professors.