Tue 16 Apr 2024 13:45 - 14:10 at Boothzaal - Talks

The need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. We propose a new explicit-state model checking algorithm for the on-the-fly verification of Linear-Time Temporal Logic (LTL) formulae that is aimed at running on such devices. We prove its correctness and termination guarantee, and experimentally compare a GPU implementation within the GPUexplore model checker with state-of-the-art CPU-based LTL model checkers. Our new algorithm is up to 150 times faster on proving the correctness of a system than the LTSmin tool running on a 32-core high-end CPU, and is more economic in using the available memory.

Tue 16 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:45 - 14:35
13:45
25m
Talk
Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking
Dutch Formal Methods Day 2024
Anton Wijs Eindhoven University of Technology
14:10
25m
Talk
Small Test Suites for Active Automata Learning
Dutch Formal Methods Day 2024