Earlier quoted context omitted.
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?
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…
This might be because it is the best combination of interactive theorem proving with automated methods that currently exists out there.