4 ms·
Interesting. I've worked concurrent systems in VHDL and Verilog (but not SystemVerilog) stacks, and those using C, C++, Haskell, OCaml, Ruby, Go, Erlang and Rus
by bayareanative 7y ago
Interesting. I've worked concurrent systems in VHDL and Verilog (but not SystemVerilog) stacks, and those using C, C++, Haskell, OCaml, Ruby, Go, Erlang and Rust.
I wonder if this approach could formally verify systems like seL4.
Here's an approach to verifying concurrent systems using coq:
https://www.sciencedirect.com/science/article/pii/S1571066108000765 https://www.sciencedirect.com/science/article/pii/S157106610...
- hwayne 7y agoYou might be interested in TLAPS, the TLA+ proof system: https://tla.msr-inria.inria.fr/tlaps/content/Home.html https://tla.msr-inria.inria.fr/tlaps/content/Home.html There's also this essay on proving TLA+ specifications in Isabelle: https://davecturner.github.io/2018/02/12/tla-in-isabelle.html https://davecturner.github.io/2018/02/12/tla-in-isabelle.htm...
- pron 7y agoThe main difference between Coq and TLA+ is that Coq is a research tool, intended and designed for use by researchers, while TLA+ is intended as an industry tool, and designed for use by engineers. They are essentially equivalent in their power when it comes to specifying and verifying software (although Coq is more suitable for proving general mathematics), but Coq is used almost exclusively by researchers. The learning curve is very different (one could get productive to the point they specify real nontrivial systems after learning TLA+ within a few days or a couple of weeks, while with Coq this takes many months), and TLA+ has much more automation.