research
NWO Veni Talent Program
Verified Analysis for Infinite-State Systems 
VAISS develops certification techniques for the analysis of infinite-state systems: systems whose behavior cannot be represented by a fixed, finite set of states, but whose correctness is still essential for trustworthy hardware, software, and AI.
Motivation
Formal verification provides mathematical guarantees that systems satisfy their specifications. In practice, however, many systems are too large or too complex to be treated as finite-state objects. They may contain counters, queues, memories, data-dependent control, recursive structure, or parameterized components. These features make verification powerful, but they also make verification results harder to trust.
The central idea of VAISS is that verification tools should not be simply trusted. Instead, they should produce independently checkable evidence. Such certificates make analysis results transparent, reproducible, and robust against implementation bugs in complex verification engines.
Research Directions
Word-Level Reasoning
Design compact proof objects for infinite-state analysis, with a focus on certificates that can be checked by small, independent validators.
Solver-Aided Checking
Reduce certificate validation to reliable automated reasoning tasks, such as SAT, SMT, or theory-specific proof checks, while keeping the trusted core small.
Abstraction and Refinement
Certify the abstraction steps that make infinite-state systems analyzable, so that scalability does not come at the cost of trust.
Tools and Benchmarks
Build prototype tooling and benchmark suites that connect certification methods to real verification workflows.
Impact
VAISS aims to make the analysis of infinite-state systems more trustworthy. This supports a verification ecosystem in which powerful tools can be used aggressively, while their results remain independently auditable.
The project builds on my work on certification for hardware model checking and extends this perspective toward richer systems, stronger specifications, and more expressive automated reasoning pipelines.
Funding
VAISS is funded by the NWO Veni Talent Programme.