About Me
My research area is in formal methods for computer science. This involves modeling and analysis of safety, dependability and security aspects of software-intensive embedded systems by means of model checking, theorem proving and automated testing.
More specifically, I am developing new model checking techniques based on symbolic techniques (e.g. abstraction, confluence, fixpoint equation systems, constraint solving) and high-performance computing (e.g. distributed model checking, multi-core and out-of-core algorithms).
Application domains include embedded systems, distributed systems, including blockchain technology, security protocols, and biological systems.
I have moved to Aarhus University by November 2018.
Expertise
Engineering & Materials Science
# Binary Decision Diagrams
# Data Structures
# Model Checking
# Petri Nets
# Specification Languages
# Temporal Logic
Mathematics
# Decision Diagrams
# Model Checking
Organisations
Publications
Recent
van de Pol, J. (2022).
Exploring a Parallel SCC Algorithm: Using TLA + and the TLC Model Checker. In T. Margaria, & B. Steffen (Eds.),
Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings (pp. 535-555). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13701 LNCS). Springer.
https://doi.org/10.1007/978-3-031-19849-6_30
Bloemen, V., Zelst, S. V., Aalst, W. V. D., Dongen, B. V.
, & Pol, J. V. D. (2022).
Aligning observed and modelled behaviour by maximizing synchronous moves and using milestones.
Information systems,
103, Article 101456.
https://doi.org/10.1016/j.is.2019.101456
Khurana, S., Schivo, S.
, Plass, J. R. M., Mersinis, N.
, Scholma, J., Kerkhofs, J.
, Zhong, L.
, van de Pol, J.
, Langerak, R., Geris, L.
, Karperien, M.
, & Post, J. N. (2021).
An ECHO of cartilage: In silico prediction of combinatorial treatments to switch between transient and permanent cartilage phenotypes with ex vivo validation.
Frontiers in bioengineering and biotechnology,
9, Article 732917.
https://doi.org/10.3389/fbioe.2021.732917
Garavel, H., Ter Beek, M. H.
, & Van De Pol, J. (2020).
The 2020 Expert Survey on Formal Methods. In M. H. ter Beek, & D. Nickovic (Eds.),
Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings (pp. 3-69). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12327 LNCS). Springer.
https://doi.org/10.1007/978-3-030-58298-2_1
Oortwijn, W.
, Huisman, M.
, Joosten, S. J. C.
, & Pol, J. V. D. (2020).
Automated Verification of Parallel Nested DFS. In A. Biere, & D. Parker (Eds.),
Tools and Algorithms for the Construction and Analysis of Systems: 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part I (pp. 247-265). (Lecture Notes in Computer Science; Vol. 12078). Springer.
https://doi.org/10.1007/978-3-030-45190-5_14
Schivo, S.
, Khurana, S.
, Govindaraj, K.
, Scholma, J., Kerkhofs, J.
, Zhong, L.
, Huang, X.
, Pol, J. V. D.
, Langerak, R., Wijnen, A. J. V., Geris, L.
, Karperien, M.
, & Post, J. N. (2020).
ECHO, the executable CHOndrocyte: A computational model to study articular chondrocytes in health and disease.
Cellular Signalling,
68, Article 109471. Advance online publication.
https://doi.org/10.1016/j.cellsig.2019.109471
Kordon, F., Leuschel, M.
, Pol, J. V. D., & Thierry-Mieg, Y. (2019).
Software Architecture of Modern Model Checkers. In B. Steffen, & G. Woeginger (Eds.),
Computing and Software Science: State of the Art and Perspectives (pp. 393-419). (Lecture Notes in Computer Science; Vol. 10000), (Theoretical Computer Science and General Issues). Springer.
https://doi.org/10.1007/978-3-319-91908-9_20
Bloemen, V., Duret-Lutz, A.
, & van de Pol, J. (2019).
Model checking with generalized Rabin and Fin-less automata.
International journal on software tools for technology transfer,
21(3), 307-324.
https://doi.org/10.1007/s10009-019-00508-4
van Dijk, T.
, Meijer, J.
, & van de Pol, J. (2019).
Multi-core On-The-Fly Saturation. In L. Zhang, & T. Vojnar (Eds.),
Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (pp. 58-75). (Lecture Notes in Computer Science; Vol. 11428), (Theoretical Computer Science and General Issues). Springer.
https://doi.org/10.1007/978-3-030-17465-1_4
André, É.
, Bloemen, V., Petrucci, L.
, & van de Pol, J. (2019).
Minimal-time synthesis for parametric timed automata. In L. Zhang, & T. Vojnar (Eds.),
Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (pp. 211-228). (Lecture Notes in Computer Science; Vol. 11428), (Theoretical Computer Science and General Issues). Springer.
https://doi.org/10.1007/978-3-030-17465-1_12
UT Research Information System
Affiliated Study Programmes
Bachelor
Master
Courses Academic Year 2023/2024
Courses in the current academic year are added at the moment they are finalised in the Osiris system. Therefore it is possible that the list is not yet complete for the whole academic year.
Courses Academic Year 2022/2023
Contact Details
Visiting Address
University of Twente
Faculty of Electrical Engineering, Mathematics and Computer Science
Building non-UT, non-campus
Drienerlolaan 5
7522NB Enschede
The Netherlands
Mailing Address
University of Twente
Faculty of Electrical Engineering, Mathematics and Computer Science
Building non-UT, non-campus
P.O. Box 217
7500 AE Enschede
The Netherlands