• Resources for a CMU Course
• CS242 from Stanford by John Mitchell
• Decision procedures lectures by Jochen Hoenicke and Andreas Podelski
• Proof Theory material
• The KeY Approach
• Decision procedures book with slides
• Language proof and logic
• The Calculus of Computation: Decision Procedures with Applications to Verification
• 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
• Introductory Course on Logic and Automata Theory by Radu Iosif
• Automata, Logic, Games and Verification by Ting Zhang
• Course and book on mathematical logic by Herbert B. Enderton
• Seminar on Artificial Intelligence Decision Procedures by Cesare Tinelli
• Automata-Theoretic Approach to Automated Verification
• 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 by Tom Ball
• Slides on abstract interpretation by David Schmidt
• CS156 at Stanford
• MIT Program Analysis Reading Group
• Patrick Cousot's MIT Class
• Introduction to Automata Theory, Languages, and Computation at Stanford
• Complexity Theory: A Modern Approach by Sanjeev Arora and Boaz Barak
• A Verifying Compiler for a Multi-threaded Object-oriented Language by Rustan Leino
• 15-815 Automated Theorem Proving by Frank Pfenning
• CSE 482 at UPenn
• Theorem proving examples by John Harrison

• The Calculus of Computation
• CSE P505 with lecture videos at University of Washington

• Statistical Data Mining Tutorials by Andrew Moore
• Machine Learning by Tommi Jaakkola

• 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

• Illustrative Risks
• Software horror stories by Nachum Deshowitz
• Inaugural Lecture by Tom Henzinger

• Software Tools for Programming Languages Research at UMD

Jahob system Berkeley Lazy Abstraction Software Verification Tool The Vampyre theorem prover written in ocaml HyTech ARMC F*ndBugs Hob system F-Rex Leak contradictor TVLA PALE Purity Analysis Kit UCLID Spec# ESC/Java2 JACK KeY KIV Spin CBMB MAGIC Daikon Saturn Chord Cascade CUTE SatAbs Comfort ObjectCheck

ASTREE AbsInt GrammaTech B-toolkit Spade CodeSurfer CoverityPrevent

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

VMCAI SAS CAV POPL PLDI TACAS CADE ESOP OOPSLA ECOOP FSE ESEC ICSE

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
• Monadic Second-Order Logic over Trees
• Semantics of guarded command language in Rustan Leino's thesis Towards Reliable Modular Programs

• Software abstractions
• 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
• Gallier Discrete Math Book Draft
• Ralph-Johan J. Back, J. Von Wright: Refinement Calculus: A Systematic Introduction

• Ocaml Resources

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

• Tutorial on OCaml Yacc

• Advice on writing from SIGPLAN
• Latex for writing mathematical formulas and list of Latex symbols
• Editing wiki

Some project ideas and Lara projects page.