- English only

# Lab for Automated Reasoning and Analysis LARA

# Resources on Software Analysis and Verification

### Related lecture notes and books

- CS242 from Stanford by John Mitchell
- Decision procedures lectures by Jochen Hoenicke and Andreas Podelski
- Lecture notes on static analysis by Michael Schwartzbach (sections 4,5,6,7 in particular)
- 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
- 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
- Complexity Theory: A Modern Approach by Sanjeev Arora and Boaz Barak
- 15-815 Automated Theorem Proving by Frank Pfenning
- CSE 482 at UPenn
- Theorem proving examples by John Harrison

- CSE P505 with lecture videos at University of Washington

- 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

### Impact

- Software horror stories by Nachum Deshowitz
- Inaugural Lecture by Tom Henzinger

### Links to tools

### Systems

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

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

### Conferences

### Notation

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

### Bibliography

- Semantics of guarded command language in Rustan Leino's thesis Towards Reliable Modular Programs

- 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))
- Ralph-Johan J. Back, J. Von Wright: Refinement Calculus: A Systematic Introduction

### Implementation Languages

### Writing documents

- Latex for writing mathematical formulas and list of Latex symbols

Some project ideas and Lara projects page.