4 ms·
Z3 is intended as more of a backend for higher-level languages, like TLA+, to use in model checking. I would be surprised if anyone were writing specs in the in
by ahelwer 6y ago
Z3 is intended as more of a backend for higher-level languages, like TLA+, to use in model checking. I would be surprised if anyone were writing specs in the input language directly.
- romac 6y agoYou nailed it, that's exactly what we use Z3 for in Apalache, a symbolic model checker for TLA+: https://apalache.informal.systems https://apalache.informal.systems
- igornotarobot 6y agoTrue. There are many frontends for Z3 that focus on various domains. For instance, those developed at Microsoft: - Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/ https://www.microsoft.com/en-us/research/project/dafny-a-lan... - Coral: https://www.microsoft.com/en-us/research/project/q-program-verifier/ https://www.microsoft.com/en-us/research/project/q-program-v... - Ivy: https://github.com/microsoft/ivy https://github.com/microsoft/ivy
- villasv 6y agoAhh, neat. Indeed, checking SAT felt a bit more generally applicable than checking SAT for temporal behaviors.