[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: Model checker and GPU
- From: Alex Weisberger <alex.m.weisberger@xxxxxxxxx>
- Date: Sun, 5 Sep 2021 20:31:35 -0700 (PDT)
- Ironport-hdrordr: A9a23:pQ9DlKzeEvTgnGKmLTlfKrPwrr1zdoMgy1knxilNoHtuA7KlfqGV7Y0mPHrP4gr5N0tQ/+xoVJPwJU80lqQFkbX5X43SOzUO0VHAROoOgeSNol2QeBEWndQtsJuIHZIOauHYPBxWjdzx5QG5F9osqeP3ipyAtKP9w3t1dw1sdshbnn9E436gYzZLbTgDPIE+EpWE4MpBun6PRVQ7B/7LeUUtbqz7vNvMm4vhYRkaQzgdyCfLow+JxdfBYmSlNjF3aUI8/Z4StVHflQr3/6OitOz+9hjm23Hu1LE+oqqR9jKGPr3+tiHDEESQtjqV
- References: <email@example.com>
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.