Anton Wijs
YOU?
Author Swipe
Preserving provability over GPU program optimizations with annotation-aware transformations Open
GPU programs are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. Such optimizations can introduce errors…
An overview of research with Slco on seamless integration of formal verification into model-driven software engineering Open
In 2009, the Simple Language of Communicating Objects (SLCO) Domain-Specific Language was designed. Since then, a range of tools have been developed around this language to conduct research on a wide range of topics, all related to the con…
Evaluating Massively Parallel Algorithms for DFA Minimisation, Equivalence Checking and Inclusion Checking Open
We study parallel algorithms for the minimisation and equivalence checking of Deterministic Finite Automata (DFAs). Regarding DFA minimisation, we implement four different massively parallel algorithms on Graphics Processing Units~(GPUs). …
GPUexplore $$^{\textsc {prob}}$$: Markov Chain State Space Construction and Verification with GPUs Open
GPUexplore $$^{\textsc {prob}}$$ is an extension of GPUexplore that constructs state spaces of Markov Chains and performs probabilistic model checking entirely on a GPU. It can construct the state space of a Discrete-Time Markov Chain and …
No Need to Be Stubborn: Partial-Order Reduction for GPU Model Checking Revisited Open
GPUexplore, a GPU-accelerated explicit-state LTL model checker, achieves significant speedups compared to sequential and multi-core CPU model checkers, but it is limited by the amount of memory available on GPUs. Partial-Order Reduction is…
An Evaluation of Massively Parallel Algorithms for DFA Minimization Open
We study parallel algorithms for the minimization of Deterministic Finite\nAutomata (DFAs). In particular, we implement four different massively parallel\nalgorithms on Graphics Processing Units (GPUs). Our results confirm the\nexpectation…
Compact Parallel Hash Tables on the GPU Open
On the GPU, hash table operation speed is determined in large part by cache line efficiency, and state-of-the-art hashing schemes thus divide tables into cache line-sized buckets. This raises the question whether performance can be further…
The fast and the capacious: memory-efficient multi-GPU accelerated explicit state space exploration with GPUexplore 3.0 Open
The GPU acceleration of explicit state space exploration, for explicit-state model checking, has been the subject of previous research, but to date, the tools have been limited in their applicability and in their practical use. Considering…
View article: HaliVer: Deductive Verification and Scheduling Languages Join Forces
HaliVer: Deductive Verification and Scheduling Languages Join Forces Open
The HaliVer tool integrates deductive verification into the popular scheduling language Halide, used for image processing pipelines and array computations. HaliVer uses Vercors, a separation logic-based verifier, to verify the correctness …
Embedding Formal Verification in Model-Driven Software Engineering with Slco: An Overview Open
In 2009, the Simple Language of Communicating Objects (Slco) Domain-Specific Language was designed. Since then, a range of tools have been developed around this language to conduct research on a wide range of topics, all related to the con…
Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking Open
The need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. In this paper, we propose a new algorithm for the on-the-fly verification of Linear-…
View article: Verifying a Radio Telescope Pipeline Using HaliVer: Solving Nonlinear and Quantifier Challenges
Verifying a Radio Telescope Pipeline Using HaliVer: Solving Nonlinear and Quantifier Challenges Open
This paper describes a case study to verify memory safety of a radio telescope pipeline, which was targeted with the PADRE project of Astron, SURF and the Netherlands eScienceCenter. As performance is important for this application, the im…
View article: $${\textsc {HaliVer}}$$: Deductive Verification and Scheduling Languages Join Forces
$${\textsc {HaliVer}}$$: Deductive Verification and Scheduling Languages Join Forces Open
The HaliVer tool integrates deductive verification into the popular scheduling language Halide , used for image processing pipelines and array computations. HaliVer uses VerCors , a separation logic-based verifier, to verify the correctnes…
Compact Parallel Hash Tables on the GPU Open
On the GPU, hash table operation speed is determined in large part by cache line efficiency, and state-of-the-art hashing schemes thus divide tables into cache line-sized buckets. This raises the question whether performance can be further…
Certified SAT solving with GPU accelerated inprocessing Open
Since 2013, the leading SAT solvers in SAT competitions all use inprocessing, which, unlike preprocessing, interleaves search with simplifications. However, inprocessing is typically a performance bottleneck, in particular for hard or larg…
GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with Data Open
GPUexplore 3.0 is an explicit state space exploration tool that runs entirely on a graphics processing unit (GPU), and supports models of concurrent systems with data variables. We discuss its workflow and modelling language, present sever…
A GPU Tree Database for Many-Core Explicit State Space Exploration Open
Various techniques have been proposed to accelerate explicit-state model checking with GPUs, but none address the compact storage of states, or if they do, at the cost of losing completeness of the checking procedure. We investigate how to…
Innermost many-sorted term rewriting on GPUs Open
This article presents a way to implement many-sorted term rewriting on a GPU. This is done by letting the GPU repeatedly perform a massively parallel evaluation of all subterms. Innermost many-sorted term rewriting is experimentally compar…
View article: Alpinist: An Annotation-Aware GPU Program Optimizer
Alpinist: An Annotation-Aware GPU Program Optimizer Open
GPU programs are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. To avoid the introduction of errors, we…
Formally Characterizing the Effect of Model Transformations on System Properties Open
In Model-Driven Software Development, models and model transformations are the primary artefacts to develop software in a structured way. Models have been subjected to formal verification for a long time, but the field of formal model tran…
Experiments of Multiple Decision Making in CDCL SAT Solvers Open
With these experiments (submission), we show that Multiple Decision Making (MDM) has a positive impact on CDCL, for many different SAT application problems when alternating between different decision queues and frequently running the WalkS…
Experiments of Multiple Decision Making in CDCL SAT Solvers Open
With these experiments (submission), we show that Multiple Decision Making (MDM) has a positive impact on CDCL, for many different SAT application problems when alternating between different decision queues and frequently running the WalkS…
A linear parallel algorithm to compute bisimulation and relational\n coarsest partitions Open
The most efficient way to calculate strong bisimilarity is by calculation the\nrelational coarsest partition on a transition system. We provide the first\nlinear time algorithm to calculate strong bisimulation using parallel random\naccess…