Model checker and GPU

[Dmitry Kulagin]

Are there tools or research projects, which use GPU to accelerate model checking of TLA+ specifications?

Thank you,

Dmitry

[Alex Weisberger]

Not exactly related, but there is the Apalache project: https://apalache.informal.systems/. This is a new model checker for TLA+ that translates a specification into an SMT-solvable constraint problem. One benefit of this is performance - SMT solvers are surprisingly fast, and they avoid exploring the state space directly as TLC does.

I think it's a very compelling idea though.