5 ms·
Have you found Coq or other formal-methods tooling useful?
by kragen 11mo ago
Have you found Coq or other formal-methods tooling useful?
- addaon 11mo agoNo, I haven't, but I want to. I haven't had the opportunity to go deep into formal methods for a work project yet, and on personal projects I've mostly played with Ada SPARK, not Coq. I've played with Coq a little (to the extent of re-implementing the linked paper for a subset of a different ISA), but there's definitely a learning curve. One of my personal benchmark projects is to implement a (fixed-maximum-size) MMM heap in a language, and convince myself it's both correct and of high performance; and I've yet to achieve that in any language, even SPARK, without leaning heavily on testing and hand-waving along with some amount of formal proof. I've written the code and comprehensive testing in various assembly languages (again, this is sort of my benchmark bring-up-a-new-platform-in-the-brain example), and I /think/ that for the way I think proving properties as invariants maintained across individual instructions maps pretty well to how I convince myself it's correct, but I haven't had the time, depth, or toolchain to really bottom any of this out.
- throw-qqqqq 11mo agoI have found huge value in CBMC and KLEE for statically verifying C code for real time safety critical embedded applications. ACL2 is also VERY powerful and capable.
- addaon 11mo agoI'd love some examples here.
- kragen 11mo agoSo would I!
- throw-qqqqq 11mo agoI can't give a good, covering answer without writing a wall of text, sorry in advance. CBMC and KLEE try to statically verify assertions in one of three outcomes: 1. Verified: No counter-example was found, that breaks the assertion(s). 2. Rejected: A counter-example was found, that makes an assertion false. 3. Tool runs forever or exhausts system resources. That means, any test/verification you can do at runtime, can be determined statically. You can use modal logics, automata, everything within practical limits. The modeling language is also just C, which simplifies things HUGELY. A very simple example can be found here: https://github.com/kokke/tiny-regex-c/blob/master/formal_verification.md https://github.com/kokke/tiny-regex-c/blob/master/formal_ver... (note, this has no specific assertions, only the ones inserted automatically by the tool, to check for run-time errors like zero division, array out of bounds etc.). For more involved examples, see https://www.cprover.org/cbmc/applications/ https://www.cprover.org/cbmc/applications/ or https://klee-se.org/publications/ https://klee-se.org/publications/
- kragen 11mo agoThat's fantastic, thanks! These sound like astounding systems.
- 11mo ago
- nextos 11mo agoI have found Isabelle very useful, and Dafny even more so. Amazon AWS uses Dafny to prove the correctness of some complex components. Then, they extract verified Java code. There are other target languages. Being based on Hoare logic, Dafny is really simple. The barrier of entry is low.