Resources on Software Analysis and Verification

  • ACM Classic Books Series, see e.g. Essays in computing science; The theory of parsing, translation, and compiling; Formal languages and their relation to automata



Theorem provers

  • Isabelle
    • Isabelle site including Isabelle binaries and sources, as well as a great tutotial for learning how to use Isabelle
    • Web interface to Isabelle and other assistants (Use only for small examples if you do not have access to actual Isabelle installation. Once you get an error during the proof you may need to logout and log in again to make sure the interface properly resets its state.)



Here are some Notes on Context-Free Grammars, which is the notation frequently used to describe the syntax of formulas and other formal languages.


Implementation Languages

Writing documents

Some project ideas and Lara projects page.