15-819M: Data, Code, Decisions

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

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 due	Euclid.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.