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.
Funding
VAISS is funded by the NWO Veni Talent Programme.