15-819M: Data, Code, Decisions

15-819M: Data, Code, Decisions (Fall 2009)
Instructor: André Platzer
Units: 12
Semester: Fall 2009
Time: Tue, Thu 1:30-2:50
Place: GHC 4301
This course is listed in Computer Science as 15-819M at Carnegie Mellon University
Java Program Analysis

Schedule

Date Lecture Assignment Reading Launch
KeY
Tue 09/08   Introduction and overview none Refresh Java basics
Thu 09/10 Propositional logic, sequent calculi, and DPLL
Tue 09/15 First-Order Logic, instances, axioms, and wizards
Thu 09/17 First-Order Logic and Herbrand's theorem
Tue 09/22 G-Week
Thu 09/24 G-Week
Tue 09/29 Equality Logic Assignment 1 due
Thu 10/01 First-Order Sequent Proving see slides
Tue 10/06 no class
Thu 10/08 no class
Tue 10/13 JML Java Modeling Language Part I see slides
Thu 10/15 JML Java Modeling Language Part II Assignment 2 due
Tue 10/20 Proving While Programs
Thu 10/22 Core OO Programs & Semantics
Tue 10/27 Core OO Proving
Thu 10/29 Proving Java Programs
Tue 11/03 Proving JML Specifications KeY Quicktour
Thu 11/05 no class Assignment 3 due
Tue 11/10 Soundness and Loop Proofs
Thu 11/12 Proving Loop Invariants
Tue 11/17 First-Order Arithmetic
Thu 11/19 Polynomials, Reals & Decisions
Tue 11/24 Instantiation-Based Proving (I) Assignment 4 dueEuclid.java KeY 1.5 beta
Thu 11/26 Thanksgiving
Tue 12/01 no class
Thu 12/03 Instantiation-Based Proving (II)

Acknowledgements: Some of the slides of this course are based on the course Software Engineering using Formal Methods by the group of Reiner Hähnle at Chalmers. Further acknowledgements go to Peter Baumgartner and Gernot Stenz for tutorial slides on Instance-Based Methods.