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

• Predicate Abstraction

• Semantics of guarded command language in the thesis Towards Reliable Modular Programs

• Ocaml Resources

• The Scala language http://www.scala-lang.org/

• Tutorial on OCaml Yacc

• Latex for writing mathematical formulas
• Editing wiki

• 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.)

Open source and freely available:

• Jahob system
• Berkeley Lazy Abstraction Software Verification Tool
• F*ndBugs
• Hob system

• Lecture notes on static analysis by Michael Schwartzbach (sections 4,5,6,7 in particular)
• Constraint solving and decision problems of first-order theories of concrete domains, by Ralf Treinen
• Notes on program analysis by Alex Aiken
• CSE 230 at UCSD
• Computer Science 357D at Stanford
• EECS 590 at University of Michigan
• PA 2005 at Tel-Aviv University
• CSE599L
• Slides by David Schmidt
• CS156 at Stanford
• http://web.mit.edu/16.399/

Please add here any additional resources that you found useful.

• M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, 2000. (suggested for more information on Chapter 1 (Propositional Logic) and 2 (Predicate Logic))
• Gallier Logic Book

• Ralph-Johan J. Back, J. Von Wright: Refinement Calculus: A Systematic Introduction