42 citations · 127 across the 17 of their papers we have counts for
18 papers
Random Generation of Small Quantitative Automata for Algorithm Debugging
Mikael Bisgaard Dahlsen-Jensen, Jaco van de Pol
Analysis algorithms for quantitative automata are complex and hard to validate. Existing approaches -- benchmarks, mutation testing, uniform random generation -- each fail to expos…
State-Space Abstractions for Parametric Timed Games
Mikael Bisgaard Dahlsen-Jensen, Laure Petrucci, Jaco van de Pol
Synthesizing controllers for real-time systems under both timing uncertainty and adversarial environments requires exploring prohibitively large symbolic state spaces. While zone i…
Controller Synthesis for Parametric Timed Games
Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci +1
We present a (semi)-algorithm to compute winning strategies for parametric timed games. Previous algorithms only synthesized constraints on the clock parameters for which the game…
Program Analysis via Multiple Context Free Language Reachability
Giovanna Kobus Conrado, Adam Husted Kjelstrøm, Andreas Pavlogiannis +1
Context-free language (CFL) reachability is a standard approach in static analyses, where the analysis question is phrased as a language reachability problem on a graph wrt a C…
Multi-variable Quantification of BDDs in External Memory using Nested Sweeping (Extended Paper)
Steffan Christ Sølvsten, Jaco van de Pol
Previous research on the Adiar BDD package has been successful at designing algorithms capable of handling large Binary Decision Diagrams (BDDs) stored in external memory. To do so…
On-The-Fly Algorithm for Reachability in Parametric Timed Games (Extended Version)
Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci +1
Parametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environmeand dep…
Predicting Memory Demands of BDD Operations using Maximum Graph Cuts (Extended Paper)
Steffan Christ Sølvsten, Jaco van de Pol
The BDD package Adiar manipulates Binary Decision Diagrams (BDDs) in external memory. This enables handling big BDDs, but the performance suffers when dealing with moderate-sized B…
Operations on Fixpoint Equation Systems
Thomas Neele, Jaco van de Pol
We study operations on fixpoint equation systems (FES) over arbitrary complete lattices. We investigate under which conditions these operations, such as substituting variables by t…
A Manifesto for Applicable Formal Methods
Mario Gleirscher, Jaco van de Pol, Jim Woodcock
Formal methods were frequently shown to be effective and, perhaps because of that, practitioners are interested in using them more often. Still, these methods are far less applied…
Proceedings First Workshop on Applicable Formal Methods
Mario Gleirscher, Jaco van de Pol, Jim Woodcock
This volume contains the proceedings of the 1st International Workshop on Applicable Formal Methods (AppFM 2021), 23 November 2021, held online as part of the 24th International Sy…
Efficient Binary Decision Diagram Manipulation in External Memory
Steffan Christ Sølvsten, Jaco van de Pol, Anna Blume Jakobsen +1
We follow up on the idea of Lars Arge to rephrase the Reduce and Apply procedures of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple ave…
Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Model Checking
Jeroen Meijer, Jaco van de Pol
We demonstrate the applicability of bandwidth and wavefront reduction algorithms to static variable ordering. In symbolic model checking event locality plays a major role in time a…
Generating and Solving Symbolic Parity Games
Gijs Kant, Jaco van de Pol
We present a new tool for verification of modal mu-calculus formulae for process specifications, based on symbolic parity games. It enhances an existing method, that first encodes…
Setting Parameters for Biological Models With ANIMO
Stefano Schivo, Jetse Scholma, Marcel Karperien +3
ANIMO (Analysis of Networks with Interactive MOdeling) is a software for modeling biological networks, such as e.g. signaling, metabolic or gene networks. An ANIMO model is essenti…
Variations on Multi-Core Nested Depth-First Search
Alfons Laarman, Jaco van de Pol
Recently, two new parallel algorithms for on-the-fly model checking of LTL properties were presented at the same conference: Automated Technology for Verification and Analysis, 201…
Boosting Multi-Core Reachability Performance with Shared Hash Tables
Alfons Laarman, Jaco van de Pol, Michael Weber
This paper focuses on data structures for multi-core reachability, which is a key component in model checking algorithms and other verification methods. A cornerstone of an efficie…
Proceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation
Lubos Brim, Jaco van de Pol
The 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2009) took place on November 4, 2009 at the Eindhoven University of Technology, in conjunct…
Distributed Branching Bisimulation Minimization by Inductive Signatures
Stefan Blom, Jaco van de Pol
We present a new distributed algorithm for state space minimization modulo branching bisimulation. Like its predecessor it uses signatures for refinement, but the refinement proces…