Model checker and GPU

54 views
Skip to first unread message

Dmitry Kulagin

unread,
Aug 29, 2021, 4:37:22 PM8/29/21
to tlaplus
Are there tools or research projects, which use GPU to accelerate model checking of TLA+ specifications?

Thank you,
Dmitry

Alex Weisberger

unread,
Sep 5, 2021, 11:31:35 PM9/5/21
to tlaplus
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.
Reply all
Reply to author
Forward
0 new messages