| 2026 | TASE | Random Generation of Small Quantitative Automata for Algorithm Debugging. | Mikael Bisgaard Dahlsen-Jensen, Jaco van de Pol |
| 2026 | VMCAI | Multi-variable Quantification of BDDs in External Memory using Nested Sweeping. | Steffan Christ Slvsten, Jaco van de Pol |
| 2025 | RC | On Exact Sizes of Minimal CNOT Circuits. | Jens Emil Christensen, Sren Fuglede Jrgensen, Andreas Pavlogiannis, Jaco van de Pol |
| 2025 | SAT | Depth-Optimal Quantum Layout Synthesis as SAT. | Anna Blume Jakobsen, Anders B. Clausen, Jaco van de Pol, Irfansha Shaik |
| 2025 | SAT | CNOT-Optimal Clifford Synthesis as SAT. | Irfansha Shaik, Jaco van de Pol |
| 2024 | ECAI | Optimal Layout-Aware CNOT Circuit Synthesis with Qubit Permutation. | Irfansha Shaik, Jaco van de Pol |
| 2024 | SAT | Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits. | Irfansha Shaik, Jaco van de Pol |
| 2024 | TACAS | On-The-Fly Algorithm for Reachability in Parametric Timed Games. | Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci, Jaco van de Pol |
| 2024 | TACAS | Fast Symbolic Computation of Bottom SCCs. | Anna Blume Jakobsen, Rasmus Skibdahl Melanchton Jrgensen, Jaco van de Pol, Andreas Pavlogiannis |
| 2023 | ATVA | Predicting Memory Demands of BDD Operations Using Maximum Graph Cuts. | Steffan Christ Slvsten, Jaco van de Pol |
| 2023 | ECOOP | Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism. | Magnus Madsen, Jaco van de Pol |
| 2023 | ICCAD | Optimal Layout Synthesis for Quantum Circuits as Classical Planning. | Irfansha Shaik, Jaco van de Pol |
| 2023 | SAT | Validation of QBF Encodings with Winning Strategies. | Irfansha Shaik, Maximilian Heisinger, Martina Seidl, Jaco van de Pol |
| 2023 | TACAS | A Truly Symbolic Linear-Time Algorithm for SCC Decomposition. | Casper Abild Larsen, Simon Meldahl Schmidt, Jesper Steensgaard, Anna Blume Jakobsen, Jaco van de Pol, Andreas Pavlogiannis |
| 2022 | ISoLA | Exploring a Parallel SCC Algorithm. | Jaco van de Pol |
| 2022 | ISoLA | Safe and Secure Future AI-Driven Railway Technologies: Challenges for Formal Methods in Railway. | Monika Seisenberger, Maurice H. ter Beek, Xiuyi Fan, Alessio Ferrari, Anne E. Haxthausen, Phillip James, Andrew Lawrence, Bas Luttik, Jaco van de Pol, Simon Wimmer |
| 2022 | TACAS | Adiar Binary Decision Diagrams in External Memory. | Steffan Christ Slvsten, Jaco van de Pol, Anna Blume Jakobsen, Mathias Weller Berg Thomasen |
| 2021 | FMICS | Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps. | Simon Thrane Hansen, Cludio Gomes, Maurizio Palmieri, Casper Thule, Jaco van de Pol, Jim Woodcock |
| 2021 | TACAS | Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata. | tienne Andr, Jaime Arias, Laure Petrucci, Jaco van de Pol |
| 2021 | TAP | A Benchmarks Library for Extended Parametric Timed Automata. | tienne Andr, Dylan Marinho, Jaco van de Pol |
| 2020 | FMICS | The 2020 Expert Survey on Formal Methods. | Hubert Garavel, Maurice H. ter Beek, Jaco van de Pol |
| 2020 | TACAS | Automated Verification of Parallel Nested DFS. | Wytse Oortwijn, Marieke Huisman, Sebastiaan J. C. Joosten, Jaco van de Pol |
| 2019 | CONCUR | Concurrent Algorithms and Data Structures for Model Checking (Invited Talk). | Jaco van de Pol |
| 2019 | FMCAD | Concurrent Chaining Hash Maps for Software Model Checking. | Freark I. van der Berg, Jaco van de Pol |
| 2019 | TACAS | Minimal-Time Synthesis for Parametric Timed Automata. | tienne Andr, Vincent Bloemen, Laure Petrucci, Jaco van de Pol |
| 2019 | TACAS | Multi-core On-The-Fly Saturation. | Tom van Dijk, Jeroen Meijer, Jaco van de Pol |
| 2018 | BPM | Maximizing Synchronization for Aligning Observed and Modelled Behaviour. | Vincent Bloemen, Sebastiaan J. van Zelst, Wil M. P. van der Aalst, Boudewijn F. van Dongen, Jaco van de Pol |
| 2018 | FMICS | Adaptive Learning for Learn-Based Regression Testing. | David Huistra, Jeroen Meijer, Jaco van de Pol |
| 2018 | FORTE | Parameter Synthesis Algorithms for Parametric Interval Markov Chains. | Laure Petrucci, Jaco van de Pol |
| 2018 | ICECCS | Layered and Collecting NDFS with Subsumption for Parametric Timed Automata. | Hoang Gia Nguyen, Laure Petrucci, Jaco van de Pol |
| 2016 | ATVA | Partial-Order Reduction for GPU Model Checking. | Thomas Neele, Anton Wijs, Dragan Bosnacki, Jaco van de Pol |
| 2016 | IFM | Symbolic Reachability Analysis of B Through ProB and LTSmin. | Jens Bendisposto, Philipp Krner, Michael Leuschel, Jeroen Meijer, Jaco van de Pol, Helen Treharne, Jorden Whitefield |
| 2016 | ISoLA | Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with Uppaal Stratego. | Waheed Ahmad, Jaco van de Pol |
| 2016 | ISoLA | RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification. | Maren Geske, Marc Jasper, Bernhard Steffen, Falk Howar, Markus Schordan, Jaco van de Pol |
| 2016 | ISoLA | Software that Meets Its Intent. | Marieke Huisman, Herbert Bos, Sjaak Brinkkemper, Arie van Deursen, Jan Friso Groote, Patricia Lago, Jaco van de Pol, Eelco Visser |
| 2016 | PPoPP | Multi-core on-the-fly SCC decomposition. | Vincent Bloemen, Alfons Laarman, Jaco van de Pol |
| 2016 | TACAS | Multi-core Symbolic Bisimulation Minimisation. | Tom van Dijk, Jaco van de Pol |
| 2015 | DSD | Green Computing: Power Optimisation of VFI-Based Real-Time Multiprocessor Dataflow Applications. | Waheed Ahmad, Philip K. F. Hlzenspies, Marille Stoelinga, Jaco van de Pol |
| 2015 | PPAM | A Distributed Hash Table for Shared Memory. | Wytse Oortwijn, Tom van Dijk, Jaco van de Pol |
| 2015 | TACAS | Sylvan: Multi-Core Decision Diagrams. | Tom van Dijk, Jaco van de Pol |
| 2015 | TACAS | LTSmin: High-Performance Language-Independent Model Checking. | Gijs Kant, Alfons Laarman, Jeroen Meijer, Jaco van de Pol, Stefan Blom, Tom van Dijk |
| 2013 | CAV | Multi-core Emptiness Checking of Timed Bchi Automata Using Inclusion Abstraction. | Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen, Jaco van de Pol |
| 2012 | ATVA | Improved Multi-Core Nested Depth-First Search. | Sami Evangelista, Alfons Laarman, Laure Petrucci, Jaco van de Pol |
| 2012 | BIBE | Modelling biological pathway dynamics with Timed Automata. | Stefano Schivo, Jetse Scholma, Brend Wanders, Ricardo A. Urquidi Camacho, Paul E. van der Vet, Marcel Karperien, Rom Langerak, Jaco van de Pol, Janine N. Post |
| 2012 | CONCUR | Efficient Modelling and Generation of Markov Automata. | Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, Marille Stoelinga |
| 2011 | ATVA | Multi-core Nested Depth-First Search. | Alfons Laarman, Rom Langerak, Jaco van de Pol, Michael Weber, Anton Wijs |
| 2011 | TACAS | Confluence Reduction for Probabilistic Systems. | Mark Timmer, Marille Stoelinga, Jaco van de Pol |
| 2010 | CAV | LTSmin: Distributed and Symbolic Reachability. | Stefan Blom, Jaco van de Pol, Michael Weber |
| 2010 | FMCAD | Boosting multi-core reachability performance with shared hash tables. | Alfons Laarman, Jaco van de Pol, Michael Weber |
| 2010 | ISoLA | UPPAAL in Practice: Quantitative Verification of a RapidIO Network. | Jiansheng Xing, Bart D. Theelen, Rom Langerak, Jaco van de Pol, Jan Tretmans, Jeroen Voeten |
| 2009 | ATVA | State Space Reduction of Linear Processes Using Control Flow Reconstruction. | Jaco van de Pol, Mark Timmer |
| 2009 | CONCUR | Compositional Control Synthesis for Partially Observable Systems. | Wouter Kuijper, Jaco van de Pol |
| 2009 | TACAS | Computing Weakest Strategies for Safety Games of Imperfect Information. | Wouter Kuijper, Jaco van de Pol |
| 2008 | ICTAC | Symbolic Reachability for Process Algebras with Recursive Data Types. | Stefan Blom, Jaco van de Pol |
| 2008 | TASE | PDL over Accelerated Labeled Transition Systems. | Taolue Chen, Jaco van de Pol, Yanjing Wang |
| 2007 | CONCUR | Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems. | Taolue Chen, Bas Ploeger, Jaco van de Pol, Tim A. C. Willemse |
| 2007 | IFM | Bug Hunting with False Negatives. | Jens R. Calam, Natalia Ioustinova, Jaco van de Pol, Natalia Sidorova |
| 2007 | TACAS | Distributed Analysis with | Stefan Blom, Jens R. Calam, Bert Lisser, Simona Orzan, Jun Pang, Jaco van de Pol, Muhammad Torabi Dashti, Anton Wijs |
| 2006 | GI | Automatisierte Erzeugung von TTCN-3 Testfillen aus UML-Modellen. | Jens R. Calam, Natalia Ioustinova, Jaco van de Pol |
| 2005 | APSEC | Data Abstraction and Constraint Solving for Conformance Testing. | Jens R. Calam, Natalia Ioustinova, Jaco van de Pol, Natalia Sidorova |
| 2005 | FMICS | Solving scheduling problems by untimed model checking: the clinical chemical analyser case study. | Anton Wijs, Jaco van de Pol, Elena M. Bortnik |
| 2005 | MFCS | A BDD-Representation for the Logic of Equality and Uninterpreted Functions. | Jaco van de Pol, Olga Tveretina |
| 2004 | SEFM | Abstraction of Parallel Uniform Processes with Data. | Jun Pang, Jaco van de Pol, Miguel Valero Espada |
| 2002 | CAV | State Space Reduction by Proving Confluence. | Stefan Blom, Jaco van de Pol |
| 2002 | CONCUR | Refinement and Verification Applied to an In-Flight Data Acquisition Unit. | Wan J. Fokkink, Natalia Ioustinova, Ernst Kesseler, Jaco van de Pol, Yaroslav S. Usenko, Yuri A. Yushtein |
| 2002 | Coordination | Formal Specification of JavaSpaces Architecture Using µCRL. | Jaco van de Pol, Miguel Valero Espada |
| 2002 | SAC | Formal verification of replication on a distributed data space architecture. | Jozef Hooman, Jaco van de Pol |
| 2001 | CAV | µCRL: A Toolset for Analysing Algebraic Specifications. | Stefan Blom, Wan J. Fokkink, Jan Friso Groote, Izak van Langevelde, Bert Lisser, Jaco van de Pol |
| 2000 | LPAR | Equational Binary Decision Diagrams. | Jan Friso Groote, Jaco van de Pol |
| 2000 | MFCS | State Space Reduction Using Partial tau-Confluence. | Jan Friso Groote, Jaco van de Pol |
| 2000 | MFCS | Binary Decision Diagrams by Shard Rewriting. | Jaco van de Pol, Hans Zantema |
| 1999 | IFM | Modular Formal Specification of Data and Behaviour. | Jaco van de Pol, Jozef Hooman, Edwin D. de Jong |
| 1998 | CONCUR | Checking Verifications of Protocols and Distributed Systems by Computer. | Jan Friso Groote, Franois Monin, Jaco van de Pol |
| 1997 | MFCS | Simulation as a Correct Transformation of Rewrite Systems. | Wan J. Fokkink, Jaco van de Pol |