4 ms·

I want to learn formal verification on my own. Do you know of any resources? I got Rolf Dreshler's book on circuit verification, but I would like to master both

I want to learn formal verification on my own. Do you know of any resources? I got Rolf Dreshler's book on circuit verification, but I would like to master both hardware and software. Would you kindly provide with some pointers?

CalChris 9y ago
It's a broad subject and I'm only interested in software verification. It's specialized enough that you should be reading papers and reading about systems. My favorite systems+papers are: Coq: The world’s best macro assembler? https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/ https://www.microsoft.com/en-us/research/publication/coq-wor... Vale: Verifying High-Performance Cryptographic Assembly Code https://project-everest.github.io/assets/vale2017.pdf https://project-everest.github.io/assets/vale2017.pdf x86proved https://x86proved.codeplex.com/ https://x86proved.codeplex.com/
mcguire 9y ago
Two schools: * Coq/dependent types. Check out Software Foundations by Benjamin Pierce, et. al. Everything's online. Also see Idris, which has a good book from Manning. * SMT-solver-based verification of existing languages. See SPARK/Ada (there's a good book but I can't remember the name presently) and the GNAT website. Also, Frama-C, although the documentation is more spotty. Then there's Rustan Leino's work on Dafny and Boogie. Oh, and Why3. And some work on verifying Java code that I haven't played with yet.
- mcguire 9y ago
  Three, three schools: * Model checking/high level formal specs. Lamport's TLA+, Alloy, possibly Z. There are some good TLA+ things online, I just couldn't get into it. (I feel bad.)
- auggierose 9y ago
  Isabelle/HOL (the one sel4 was done in) appears in none of your two schools ... This might be because it is the best combination of interactive theorem proving with automated methods that currently exists out there.
  - mcguire 9y ago
    As far as I know, Isabelle/HOL is fairly similar to Coq, perhaps with more automation. If there is something like Software Foundations for Isabelle, I'd be slobbering all over myself in excitement to hear about it. (And I'm still a little confused about how the C code of seL4 is verified against the formal specs. Is there something like Frama-C involved?)
    - auggierose 9y ago
      Both are interactive theorem provers, so yeah. But the two school comment said Coq/dependent-types, and Isabelle/HOL is neither Coq, nor does it do dependent types :) If you are looking for developments in Isabelle/HOL, there is the AFP: https://www.isa-afp.org/ https://www.isa-afp.org/ There is also a recent book that might interest you: http://www.concrete-semantics.org/ http://www.concrete-semantics.org/
      - mcguire 9y ago
        Sweet, thanks!

CalChris 9y ago

It's a broad subject and I'm only interested in software verification. It's specialized enough that you should be reading papers and reading about systems. My favorite systems+papers are: Coq: The world’s best macro assembler? https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/ https://www.microsoft.com/en-us/research/publication/coq-wor... Vale: Verifying High-Performance Cryptographic Assembly Code https://project-everest.github.io/assets/vale2017.pdf https://project-everest.github.io/assets/vale2017.pdf x86proved https://x86proved.codeplex.com/ https://x86proved.codeplex.com/

mcguire 9y ago

Two schools: * Coq/dependent types. Check out Software Foundations by Benjamin Pierce, et. al. Everything's online. Also see Idris, which has a good book from Manning. * SMT-solver-based verification of existing languages. See SPARK/Ada (there's a good book but I can't remember the name presently) and the GNAT website. Also, Frama-C, although the documentation is more spotty. Then there's Rustan Leino's work on Dafny and Boogie. Oh, and Why3. And some work on verifying Java code that I haven't played with yet.

mcguire 9y ago
Three, three schools: * Model checking/high level formal specs. Lamport's TLA+, Alloy, possibly Z. There are some good TLA+ things online, I just couldn't get into it. (I feel bad.)
auggierose 9y ago
Isabelle/HOL (the one sel4 was done in) appears in none of your two schools ... This might be because it is the best combination of interactive theorem proving with automated methods that currently exists out there.
- mcguire 9y ago
  As far as I know, Isabelle/HOL is fairly similar to Coq, perhaps with more automation. If there is something like Software Foundations for Isabelle, I'd be slobbering all over myself in excitement to hear about it. (And I'm still a little confused about how the C code of seL4 is verified against the formal specs. Is there something like Frama-C involved?)
  - auggierose 9y ago
    Both are interactive theorem provers, so yeah. But the two school comment said Coq/dependent-types, and Isabelle/HOL is neither Coq, nor does it do dependent types :) If you are looking for developments in Isabelle/HOL, there is the AFP: https://www.isa-afp.org/ https://www.isa-afp.org/ There is also a recent book that might interest you: http://www.concrete-semantics.org/ http://www.concrete-semantics.org/
    - mcguire 9y ago
      Sweet, thanks!