Prof. Jaco van de Pol

My Publications in DBLP and Google Scholar.

Full Curriculum Vitae (July 2024, pdf)

Research Interests

Modeling and analysis of safety, dependability, performance, and security aspects of software-intensive embedded systems by means of
- model checking,
- automated planning,
- theorem proving, and
- automated testing.
Synthesis of parameters and strategies, schedules and plans, for the control and testing of safety-critical systems.
The development of new model checking techniques based on
- symbolic techniques (e.g. abstraction, confluence, fixpoint equation systems, constraint solving); and
- high-performance graph algorithms (e.g. distributed and multi-core model checking algorithms).
Application domains include
- embedded systems (e.g., railway safety, interlockings),
- distributed systems (e.g., blockchain and smart contracts),
- security protocols and risk analysis (e.g., through attack-defense trees),
- energy optimization (e.g. through stochastic timed automata),
- signaling pathways in biological systems (e.g., through timed automata); and
- quantum circuit optimization and compilation (e.g., through planning and SAT solving).

I am teaching a 10EC course on Computability and Logic.
I am teaching a 10 EC course on Algorithmic Model Checking with Andreas Pavlogiannis.

Are you interested in the Computer Science BSc programmes or MSc programmes?
See our Graduate School for PhD opportunities in Computer Science at Aarhus University.

Editorial board SCP (Science of Computer Programming)
Editorial board STTT (Software Tools and Technology Transfer)
Member of the Steering Committee SPIN Symposium on Model Checking Software
Member (Chair 2018-2022) of the Steering Committee of FMICS, the ERCIM working group on Formal Methods in Industrial Critical Systems
PC co-chair of appFM 2021, 1st IW on Applicable Formal Methods (Beijing, China), with Mario Gleirscher and Jim Woodcock. Proceedings available as: EPTCS 349
Organizer of the Lorentz Workshop on Verification Competitions, Feb 2019, Leiden, The Netherlands
Program Chair of appFM 2021, SynCop 2019, TACAS 2015 (tool chair), AVOCS 2014, and SPIN 2010.
PC member of:
- TACAS (2021, 2020, 2017, 2015, 2014)
- FM 2021, FM World Congress 2019, Doctoal Symposium (2019, 2016)
- FMICS (2024 2023, 2022, 2021, 2020, 2019, 2018, 2017, 2016, 2015, 2014)
- ICFEM (2020, 2019, 2018, 2017, 2016, 2015, 2014)
- SPIN ( 2024, 2022, 2021, 2019, 2018, 2015, 2014)
- AVOCS (2017, 2016, 2015, 2014)
- SETTA (2021, 2020, 2019)
- Petri Nets (2023, 2022, 2021)
- ACSD (2019, 2018, 2017)
- TASE 2023, iFM 2022, CONCUR 2021, FORTE 2019, FSCD 2019, SBMF 2019, FMCAD 2018, SynCop 2018, TMPA 2017, LATA 2015.

With Magnus Madsen as PI, we received a 60,000 USD Amazon Research Award for our research on Type Inference with Boolean Unification in Flix
We won the Oded Maler best paper Award 2020 at FORMATS 2020 (Vienna) with Simon Wimmer and Frédéric Herbreteau
We published The 2020 Expert Survey on Formal Methods with Hubert Garavel and Maurice ter Beek
Invited Lecturer at FSTTCS tutorial Advances in Verification, Bits-Pilani, Goa, India, 2020
Invited Speaker at CONCUR 2019, Concurrency Theory, Amsterdam, The Netherlands
Best Student Paper Award at BPM 2018, Sydney Australia, with Vincent Bloemen, et al.
Best Paper Award at SPIN 2017, Santa Barbara, USA, with Wytse Oortwijn, et al.
Simon Wimmer won a H2020 MSCA Individual Fellowship in Aarhus, for his project "Certywhere" - Safe Real-Time Systems: Certification Everywhere.
My PhD students Vincent Bloemen and Marcus Gerhold win the VERSEN PhD Thesis Award 2020
May 2019: Nominated for the best teacher award at CS@Aarhus for my course on Computability & Logic
Two papers at TACAS 2019, both with Artefact Evaluation Stamp
Djurre van der Wal wins the Internet MSc thesis prize 2018.
I came to Aarhus University by November 1st, 2018