Jaco van de Pol

Orcid: 0000-0003-4305-0625

Affiliations:
  • Aarhus University, Department of Computer Science, Aarhus, Denmark
  • University of Twente, Enschede, Netherlands


According to our database1, Jaco van de Pol authored at least 185 papers between 1993 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Optimal Layout Synthesis for Deep Quantum Circuits on NISQ Processors with 100+ Qubits.
CoRR, 2024

On-The-Fly Algorithm for Reachability in Parametric Timed Games (Extended Version).
CoRR, 2024

Fast Symbolic Computation of Bottom SCCs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

On-The-Fly Algorithm for Reachability in Parametric Timed Games.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

2023
A manifesto for applicable formal methods.
Softw. Syst. Model., December, 2023

Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems.
Proc. ACM Program. Lang., October, 2023

Predicting Memory Demands of BDD Operations using Maximum Graph Cuts (Extended Paper).
CoRR, 2023

Search-Space Pruning with Int-Splits for Faster QBF Solving.
CoRR, 2023

Operations on Fixpoint Equation Systems.
CoRR, 2023

Concise QBF Encodings for Games on a Grid (extended version).
CoRR, 2023

Implicit State and Goals in QBF Encodings for Positional Games (extended version).
CoRR, 2023

A Truly Symbolic Linear-Time Algorithm for SCC Decomposition.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Validation of QBF Encodings with Winning Strategies.
Proceedings of the 26th International Conference on Theory and Applications of Satisfiability Testing, 2023

Adiar 1.1 - Zero-Suppressed Decision Diagrams in External Memory.
Proceedings of the NASA Formal Methods - 15th International Symposium, 2023

Optimal Layout Synthesis for Quantum Circuits as Classical Planning.
Proceedings of the IEEE/ACM International Conference on Computer Aided Design, 2023

Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism.
Proceedings of the 37th European Conference on Object-Oriented Programming, 2023

Predicting Memory Demands of BDD Operations Using Maximum Graph Cuts.
Proceedings of the Automated Technology for Verification and Analysis, 2023

Implicit QBF Encodings for Positional Games.
Proceedings of the Advances in Computer Games - 18th International Conference, 2023

2022
Verification and synthesis of co-simulation algorithms subject to algebraic loops and adaptive steps.
Int. J. Softw. Tools Technol. Transf., 2022

Aligning observed and modelled behaviour by maximizing synchronous moves and using milestones.
Inf. Syst., 2022

Adiar Binary Decision Diagrams in External Memory.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Safe and Secure Future AI-Driven Railway Technologies: Challenges for Formal Methods in Railway.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Practice, 2022

Exploring a Parallel SCC Algorithm.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 2022

Efficient Convex Zone Merging in Parametric Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2022

Classical Planning as QBF without Grounding.
Proceedings of the Thirty-Second International Conference on Automated Planning and Scheduling, 2022

2021
Relational nullable types with Boolean unification.
Proc. ACM Program. Lang., 2021

Classical Planning as QBF without Grounding (extended version).
CoRR, 2021

Efficient Binary Decision Diagram Manipulation in External Memory.
CoRR, 2021

A Benchmarks Library for Extended Parametric Timed Automata.
Proceedings of the Tests and Proofs - 15th International Conference, 2021

Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps.
Proceedings of the Formal Methods for Industrial Critical Systems, 2021

Synthesizing Co-Simulation Algorithms with Step Negotiation and Algebraic Loop Handling.
Proceedings of the Annual Modeling and Simulation Conference, 2021

2020
Polymorphic types and effects with Boolean unification.
Proc. ACM Program. Lang., 2020

On Completeness of Liveness Synthesis for Parametric Timed Automata (Extended Abstract).
Proceedings of the Recent Trends in Algebraic Development Techniques, 2020

Automated Verification of Parallel Nested DFS.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Certifying Emptiness of Timed Büchi Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2020

The 2020 Expert Survey on Formal Methods.
Proceedings of the Formal Methods for Industrial Critical Systems, 2020

2019
Software Architecture of Modern Model Checkers.
Proceedings of the Computing and Software Science - State of the Art and Perspectives, 2019

Model checking with generalized Rabin and Fin-less automata.
Int. J. Softw. Tools Technol. Transf., 2019

Sound black-box checking in the LearnLib.
Innov. Syst. Softw. Eng., 2019

Multi-core On-The-Fly Saturation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Minimal-Time Synthesis for Parametric Timed Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Concurrent Chaining Hash Maps for Software Model Checking.
Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

Concurrent Algorithms and Data Structures for Model Checking (Invited Talk).
Proceedings of the 30th International Conference on Concurrency Theory, 2019

2018
MCC'2017 - The Seventh Model Checking Contest.
Trans. Petri Nets Other Model. Concurr., 2018

Multi-core symbolic bisimulation minimisation.
Int. J. Softw. Tools Technol. Transf., 2018

Layered and Collecting NDFS with Subsumption for Parametric Timed Automata.
Proceedings of the 23rd International Conference on Engineering of Complex Computer Systems, 2018

Parameter Synthesis Algorithms for Parametric Interval Markov Chains.
Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2018

Adaptive Learning for Learn-Based Regression Testing.
Proceedings of the Formal Methods for Industrial Critical Systems, 2018

Maximizing Synchronization for Aligning Observed and Modelled Behaviour.
Proceedings of the Business Process Management - 16th International Conference, 2018

Synchronous or Alternating? - LTL Black-Box Checking of Mealy Machines by Combining the LearnLib and LTSmin.
Proceedings of the Models, Mindsets, 2018

Symbolically Aligning Observed and Modelled Behaviour.
Proceedings of the 18th International Conference on Application of Concurrency to System Design, 2018

Multi-core Decision Diagrams.
Proceedings of the Handbook of Parallel Constraint Reasoning., 2018

Parallel Model Checking Algorithms for Linear-Time Temporal Logic.
Proceedings of the Handbook of Parallel Constraint Reasoning., 2018

2017
Sylvan: multi-core framework for decision diagrams.
Int. J. Softw. Tools Technol. Transf., 2017

Distributed binary decision diagrams for symbolic reachability.
Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

The RERS 2017 challenge and workshop (invited paper).
Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

Explicit state model checking with generalized Büchi and Rabin automata.
Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 2017

Improving the Timed Automata Approach to Biological Pathway Dynamics.
Proceedings of the Models, Algorithms, Logics and Tools, 2017

Property-Preserving Generation of Tailored Benchmark Petri Nets.
Proceedings of the 17th International Conference on Application of Concurrency to System Design, 2017

2016
Confluence reduction for Markov automata.
Theor. Comput. Sci., 2016

Guard-based partial-order reduction.
Int. J. Softw. Tools Technol. Transf., 2016

Preface of Special issue on Automated Verification of Critical Systems (AVoCS'14).
Sci. Comput. Program., 2016

Modelling with ANIMO: between fuzzy logic and differential equations.
BMC Syst. Biol., 2016

Multi-core on-the-fly SCC decomposition.
Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2016

Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Reachability Analysis.
Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Software that Meets Its Intent.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with Uppaal Stratego.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016

Symbolic Reachability Analysis of B Through ProB and LTSmin.
Proceedings of the Integrated Formal Methods - 12th International Conference, 2016

Multi-core SCC-Based LTL Model Checking.
Proceedings of the Hardware and Software: Verification and Testing, 2016

Partial-Order Reduction for GPU Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2016

Model Checking and Evaluating QoS of Batteries in MPSoC Dataflow Applications via Hybrid Automata.
Proceedings of the 16th International Conference on Application of Concurrency to System Design, 2016

2015
Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Model Checking.
CoRR, 2015

Modeling and Verification of the Bitcoin Protocol.
Proceedings of the Proceedings Workshop on Models for Formal Analysis of Real Systems, 2015

LTSmin: High-Performance Language-Independent Model Checking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Sylvan: Multi-Core Decision Diagrams.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

A Distributed Hash Table for Shared Memory.
Proceedings of the Parallel Processing and Applied Mathematics, 2015

Automated Verification of Nested DFS.
Proceedings of the Formal Methods for Industrial Critical Systems, 2015

Green Computing: Power Optimisation of VFI-Based Real-Time Multiprocessor Dataflow Applications.
Proceedings of the 2015 Euromicro Conference on Digital System Design, 2015

2014
Modeling Biological Pathway Dynamics With Timed Automata.
IEEE J. Biomed. Health Informatics, 2014

Thoughtful brute-force attack of the RERS 2012 and 2013 Challenges.
Int. J. Softw. Tools Technol. Transf., 2014

Preface.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2014

Setting Parameters for Biological Models With ANIMO.
Proceedings of the Proceedings 1st International Workshop on Synthesis of Continuous Parameters, 2014

Generating and Solving Symbolic Parity Games.
Proceedings of the Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering, 2014

Read, Write and Copy Dependencies for Symbolic Model Checking.
Proceedings of the Hardware and Software: Verification and Testing, 2014

Lace: Non-blocking Split Deque for Work-Stealing.
Proceedings of the Euro-Par 2014: Parallel Processing Workshops, 2014

Resource-Constrained Optimal Scheduling of Synchronous Dataflow Graphs via Timed Automata.
Proceedings of the 14th International Conference on Application of Concurrency to System Design, 2014

2013
Guard-Based Partial-Order Reduction.
Proceedings of the Model Checking Software - 20th International Symposium, 2013

Confluence Reduction for Markov Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2013

Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012
A linear process-algebraic format with data for probabilistic automata.
Theor. Comput. Sci., 2012

Multi-Core BDD Operations for Symbolic Reachability.
Proceedings of the Proceedings the Sixth International Workshop on the Practical Application of Stochastic Modelling, 2012

Multi-core and/or Symbolic Model Checking.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012

Efficient Instantiation of Parameterised Boolean Equation Systems to Parity Games
Proceedings of the Proceedings First Workshop on GRAPH Inspection and Traversal Engineering, 2012

Multi-core Reachability for Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2012

Efficient Modelling and Generation of Markov Automata.
Proceedings of the CONCUR 2012 - Concurrency Theory - 23rd International Conference, 2012

Modelling biological pathway dynamics with Timed Automata.
Proceedings of the 12th IEEE International Conference on Bioinformatics & Bioengineering, 2012

Improved Multi-Core Nested Depth-First Search.
Proceedings of the Automated Technology for Verification and Analysis, 2012

2011
A calculus for four-valued sequential logic.
Theor. Comput. Sci., 2011

On the axiomatizability of priority II.
Theor. Comput. Sci., 2011

Distributed Algorithms for SCC Decomposition.
J. Log. Comput., 2011

Variations on Multi-Core Nested Depth-First Search
Proceedings of the Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, 2011

Confluence Reduction for Probabilistic Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Parallel Recursive State Compression for Free.
Proceedings of the Model Checking Software, 2011

Multi-Core LTSmin: Marrying Modularity and Scalability.
Proceedings of the NASA Formal Methods, 2011

Multi-core Nested Depth-First Search.
Proceedings of the Automated Technology for Verification and Analysis, 2011

2010
Towards model checking executable UML specifications in mCRL2.
Innov. Syst. Softw. Eng., 2010

Confluence Reduction for Probabilistic Systems (extended version)
CoRR, 2010

UPPAAL in Practice: Quantitative Verification of a RapidIO Network.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

Automated Verification of Executable UML Models.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010

Boosting multi-core reachability performance with shared hash tables.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

LTSmin: Distributed and Symbolic Reachability.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

From POOSL to UPPAAL: Transformation and Quantitative Analysis.
Proceedings of the 10th International Conference on Application of Concurrency to System Design, 2010

A Linear Process-Algebraic Format for Probabilistic Systems with Data.
Proceedings of the 10th International Conference on Application of Concurrency to System Design, 2010

2009
Solving scheduling problems by untimed model checking.
Int. J. Softw. Tools Technol. Transf., 2009

Distributed Branching Bisimulation Minimization by Inductive Signatures
Proceedings of the Proceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation, 2009

Computing Weakest Strategies for Safety Games of Imperfect Information.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Compositional Control Synthesis for Partially Observable Systems.
Proceedings of the CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009

State Space Reduction of Linear Processes Using Control Flow Reconstruction.
Proceedings of the Automated Technology for Verification and Analysis, 2009

2008
Simulated time for host-based testing with TTCN-3.
Softw. Test. Verification Reliab., 2008

Applying formal methods to gossiping networks with mCRL and groove.
SIGMETRICS Perform. Evaluation Rev., 2008

A Multi-Core Solver for Parity Games.
Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation, 2008

Distributed Markovian Bisimulation Reduction aimed at CSL Model Checking.
Proceedings of the 7th International Workshop on Parallel and Distributed Methods in verifiCation, 2008

Mechanical Verification of a Two-Way Sliding Window Protocol.
Proceedings of the thirty-first Communicating Process Architectures Conference, 2008

PDL over Accelerated Labeled Transition Systems.
Proceedings of the Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, 2008

Applying Model-Based Testing to HTML Rendering Engines - A Case Study.
Proceedings of the Testing of Software and Communicating Systems, 2008

Leader Election in Anonymous Rings: Franklin Goes Probabilistic.
Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

Symbolic Reachability for Process Algebras with Recursive Data Types.
Proceedings of the Theoretical Aspects of Computing, 2008

A Typical Verification Challenge for the GRID.
Proceedings of the Distributed Verification and Grid Computing, 10.08. - 14.08.2008, 2008

2007
Generalizing DPLL and satisfiability for equalities.
Inf. Comput., 2007

An abstract interpretation toolkit for µCRL.
Formal Methods Syst. Des., 2007

A Database Approach to Distributed State Space Generation.
Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation, 2007

Improved Distributed Algorithms for SCC Decomposition.
Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation, 2007

Distributed Analysis with <i>mu</i> CRL: A Compendium of Case Studies.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Bug Hunting with False Negatives.
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems.
Proceedings of the CONCUR 2007 - Concurrency Theory, 18th International Conference, 2007

2006
Distribution of a Simple Shared Dataspace Architecture.
Fundam. Informaticae, 2006

Cones and foci: A mechanical framework for protocol verification.
Formal Methods Syst. Des., 2006

Automatisierte Erzeugung von TTCN-3 Testfiällen aus UML-Modellen.
Proceedings of the 36. Jahrestagung der Gesellschaft für Informatik, 2006

TTCN-3 for Distributed Testing Embedded Software.
Proceedings of the Perspectives of Systems Informatics, 2006

TTCN-3 Testing of Hoorn-Kersenboogerd Railway Interlocking.
Proceedings of the Canadian Conference on Electrical and Computer Engineering, 2006

Accelerated Modal Abstractions of Labelled Transition Systems.
Proceedings of the Algebraic Methodology and Software Technology, 2006

2005
Semantic models of a timed distributed dataspace architecture.
Theor. Comput. Sci., 2005

Introductory paper.
Int. J. Softw. Tools Technol. Transf., 2005

Verification of a sliding window protocol in µCRL and PVS.
Formal Aspects Comput., 2005

Preface.
Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference, 2005

Preface.
Proceedings of the 4th International Workshop on Parallel and Distributed Methods in Verification, 2005

Automatic Model-Based Generation of Parameterized Test Cases Using Data Abstraction.
Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference, 2005

Zero, successor and equality in BDDs.
Ann. Pure Appl. Log., 2005

Generalized Innermost Rewriting.
Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

A BDD-Representation for the Logic of Equality and Uninterpreted Functions.
Proceedings of the Mathematical Foundations of Computer Science 2005, 2005

Solving scheduling problems by untimed model checking: the clinical chemical analyser case study.
Proceedings of the 10th international workshop on Formal methods for industrial critical systems, 2005

Simulated Time for Testing Railway Interlockings with TTCN-3.
Proceedings of the Formal Approaches to Software Testing, 5th International Workshop, 2005

Data Abstraction and Constraint Solving for Conformance Testing.
Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), 2005

2004
Introductory paper.
Int. J. Softw. Tools Technol. Transf., 2004

An Abstract Interpretation Toolkit for <i>mu</i>CRL.
Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems, 2004

A State Space Distribution Policy Based on Abstract Interpretation.
Proceedings of the 3rd International Workshop on Parallel and Distributed Methods in Verification, 2004

Abstraction of Parallel Uniform Processes with Data.
Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004

Modal Abstractions in µCRL.
Proceedings of the Algebraic Methodology and Software Technology, 2004

Verifying a Sliding Window Protocol in µCRL.
Proceedings of the Algebraic Methodology and Software Technology, 2004

2003
New developments around the mCRL tool set.
Proceedings of the Eighth International Workshop on Formal Methods for Industrial Critical Systems, 2003

Verification of Distributed Dataspace Architectures.
Proceedings of the Perspectives of Systems Informatics, 2003

Verification of JavaSpaces<sup>TM</sup> Parallel Programs.
Proceedings of the 3rd International Conference on Application of Concurrency to System Design (ACSD 2003), 2003

2002
Formal verification of replication on a distributed data space architecture.
Proceedings of the 2002 ACM Symposium on Applied Computing (SAC), 2002

JITty: A Rewriter with Strategy Annotations.
Proceedings of the Rewriting Techniques and Applications, 13th International Conference, 2002

Equivalent Semantic Models for a Distributed Dataspace Architecture.
Proceedings of the Formal Methods for Components and Objects, 2002

Formal Specification of JavaSpaces Architecture Using µCRL.
Proceedings of the Coordination Models and Languages, 5th International Conference, 2002

Refinement and Verification Applied to an In-Flight Data Acquisition Unit.
Proceedings of the CONCUR 2002, 2002

State Space Reduction by Proving Confluence.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
Just-in-time: On Strategy Annotations.
Proceedings of the 1st International Workshop on Reduction Strategies in Rewriting and Programming, 2001

A rewriting approach to binary decision diagrams.
J. Log. Algebraic Methods Program., 2001

µCRL: A Toolset for Analysing Algebraic Specifications.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000
Binary Decision Diagrams by Shard Rewriting.
Proceedings of the Mathematical Foundations of Computer Science 2000, 2000

State Space Reduction Using Partial tau-Confluence.
Proceedings of the Mathematical Foundations of Computer Science 2000, 2000

Equational Binary Decision Diagrams.
Proceedings of the Logic for Programming and Automated Reasoning, 2000

Refinement in Requirements Specification and Analysis: A Case Study.
Proceedings of the 7th IEEE International Symposium on Engineering of Computer-Based Systems (ECBS 2000), 2000

1999
Modular Formal Specification of Data and Behaviour.
Proceedings of the Integrated Formal Methods, 1999

1998
Operational Semantics of Rewriting with Priorities.
Theor. Comput. Sci., 1998

Checking Verifications of Protocols and Distributed Systems by Computer.
Proceedings of the CONCUR '98: Concurrency Theory, 1998

1997
Simulation as a Correct Transformation of Rewrite Systems.
Proceedings of the Mathematical Foundations of Computer Science 1997, 1997

1996
A Bounded Retransmission Protocol for Large Data Packets.
Proceedings of the Algebraic Methodology and Software Technology, 1996

1995
Strict Functionals for Termination Proofs.
Proceedings of the Typed Lambda Calculi and Applications, 1995

Two <i>Different</i> Strong Normalization Proofs?
Proceedings of the Higher-Order Algebra, 1995

1993
Termination Proofs for Higher-order Rewrite Systems.
Proceedings of the Higher-Order Algebra, 1993


  Loading...