[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: Model checker and GPU
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.
On Sunday, August 29, 2021 at 4:37:22 PM UTC-4 dmitry....@xxxxxxxxx wrote:
Are there tools or research projects, which use GPU to accelerate model checking of TLA+ specifications?
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b0f851d6-9d1c-423e-b344-8d9baeacc352n%40googlegroups.com.