Prof. Jaco van de Pol

Department of Computer Science Aarhus University Contact Information Research Interests Teaching My Publications in DBLP and Google Scholar. Full Curriculum Vitae (May 2025, pdf)

Recent News

• My PhD project "QoptiQ: Quest for Optimal Quantum Circuits" got approved by the Danish Quantum Algorithms Acadamy in DEiC.
• Two papers accepted at SAT 2025, one on Clifford Circuit Synthesis, and one on Depth-Optimal Quantum Layout Synthesis, and one paper at RC 2025 on Optimal CNOT synthesis
• Together with Andreas Pavlogiannis, we will organize CONFEST 2025 in Aarhus!
• Distinguished Paper Award at ECOOP 2023 with Magnus Madsen for "Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism"
• Outstanding Domain Submission Award at IPC 2023 with Irfansha Shaik for the domain "Quantum Circuit Layout Synthesis".
• Our project "Automated Planning for Quantum Circuit Optimization" got approved by Innovationsfonden Denmark. After his PhD defense, Irfansha Shaik has started as a postdoc at Kvantify.
• I was joint invited speaker at CONCUR+FORMATS+FMICS, Antwerpen, 2023
• PC member of FM 2026, 27th Formal Methods Symposium, Tokyo, Japan
• PC member of ECAI 2025, 28th European Conference on Artificial Intelligence, Bologna, Italy
• PC member of NFM 2025, NASA Formal Methods Symposium, NASA Langley Research Center
• PC member of FMICS 2024, 29th International Conference on Formal Methods for Industrial Critical Systems, Milan, Italy
• PC member of SPIN 2024, 30th International Symposium on Model Checking Software, Luxembourg
• PC member of TASE 2023, International Conference on Model Checking Software, Bristol, UK.
• PC member of Petri Nets 2023, International Conference on Concurrency Theory, Lisbon, Portugal.
• PC member of CONCUR 2021, International Conference on Concurrency Theory, Paris, France.
• PC member of FM 2021, Formal Methods, Beijing, China.
• PC member of TACAS 2021, Tools and Algorithms for the Construction and Analysis of Systems, Luxembourg.

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).

Teaching (BSc, MSc, PhD)

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

Academic Service (since 2014)

• 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.

Older News

• 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