The following is a tentative schedule of this semester's program. We will try to send a mail at the beginning of each week to give your some information about the current week's contents.

Monday 14:15 | INR 113 | Lecture 01: Introduction and Presburger Arithmetic |

Monday 16:15 | INR 113 | Labs 01: Introduction to proofs in Stainless |

Friday 13:15 | INF 119 | Exercises 01: Logic, sets, and relations |

Monday 14:15 | INR 113 | Lecture 02: Complete QE for PA. From Programs to Formulas |

Monday 16:15 | INR 113 | Labs 02: More proofs in Stainless |

Friday 13:15 | INF 119 | Lecture 03: Verification-Condition Generation for Imperative Code |

Monday 14:15 | INR 113 | Lecture 04: Weakest Preconditions and Strongest Postconditions |

Monday 16:15 | INR 113 | Termination Checking in Stainless |

Friday 13:15 | INF 119 | Lecture 05: Computing Postconditions and Preconditions |

Monday 14:15 | INR 113 | Lecture 06: Loops and Recursion |

Monday 16:15 | INR 113 | Labs 03: Proofs in Welder |

Friday 13:15 | INF 119 | Labs 03: Proofs in Welder (cont.) |

Monday 14:15 | INR 113 | Lecture 07: More Recursion. Bounded Model Checking, k-Induction, Idea of Abstract Interpretation |

Monday 16:15 | INR 113 | Labs 03: Proofs in Welder (cont.) |

Friday 13:15 | INF 119 | Exercises 03: Loop Semantics and Proofs |

Monday 14:15 | INR 113 | Lecture 08: Lattices and Abstract Interpretation |

Monday 16:15 | INR 113 | Labs 03: Proofs in Welder (end) |

Friday 13:15 | INF 119 | Lecture 09: Lattices and Abstract Interpretation (cont.) |

Monday 14:15 | INR 113 | Lecture 10: Galois Connection and Abstract Interpretation |

Monday 16:15 | INR 113 | Project Suggestions |

Friday 13:15 | INF 119 | Lecture 11: Widening/Narrowing, Invariants, and Stainless Proofs |

Monday 14:15 | INR 113 | QUIZ |

Monday 16:15 | INR 113 | QUIZ |

Friday 13:15 | INF 119 | Holiday |

**Quizzes from previous years:**

Monday 14:15 | INR 113 | Lecture 12: Synthesis from Relations and Types |

Monday 16:15 | INR 113 | Labs: Working on Projects |

Friday 13:15 | INF 119 | Lecture 13: Verifying Higher-Order Functions and Repair |

Monday 14:15 | INR 113 | Lecture 14: Resolution Theorem Proving |

Monday 16:15 | INR 113 | Labs: Working on Projects |

Friday 13:15 | INF 119 | Paper presentations: (Olivier Blanvillain) Automatic Verification of Dafny Programs with Traits, R. Ahmadi, R, Leino, J. Nummenmaa, ECOOP 2015, and (Rodrigo Raya) The use of machines to assist in rigorous proof, R. Milner, 1984 |

Monday 14:15 | INR 113 | Paper presentations: (Romain Ruetschi) Efficient E-Matching for SMT Solvers, L, Moura, N. Bjorner, CADE 2007, and (Romain Beguet) Isabelle: The Next 700 Theorem Provers, L. Paulson, 1993 |

Monday 16:15 | INR 113 | Labs: Working on Projects |

Friday 13:15 | INF 119 | Paper presentations: (Junze Bao and Dennis van der Bij) Hindley-Milner Elaboration in Applicative Style, F. Pottier, ICFP 2014, and Directly-Executable Earley Parsing, J. Aycock and N. Horspool, CC 2001 |

Monday 14:15 | INR 113 | Paper presentations: (David Aksun) CodeHint: Dynamic and Interactive Synthesis of Code Snippets, J. Galenson, P. Reames, R. Bodik, B. Hartmann, K. Sen, ICSE 2014 |

Monday 16:15 | INR 113 | Labs: Working on Projects |

Friday 13:15 | INF 119 | Paper presentations: (Marius Rosset and Florian Poma) Scalable Propagation-Based Call Graph Construction Algorithms, F. Tip, J. Palsberg, OOPSLA 2000 |

Monday 14:15 | INR 113 | Paper presentations: (Florian Alonso and Damien Doy) Demand Interprocedural Dataflow Analysis, S. Horwitz, T. Reps, and M. Sagiv, SIGSOFT 1995, and Fine-grained Caching of Verification Results, R. Leino and V. Wüstholz, CAV 2015 |

Monday 16:15 | INR 113 | Labs: Working on Projects |

Friday 13:15 | INF 119 | Last Lecture: Finish Resolution. WS1S |

Monday 14:15 | INR 113 | Project Presentations |

Friday 13:15 | INF 119 | Project Presentations |

**Grading**. The course uses *continuous control* and there is no sit-in exam in the post-semester exam period. The instructor assigns the grade based on the following:

- 40% a mid-term exam, given on
**Monday, Apr. 10, 14:15**; - 15% individually solved practical assignments (first quarter);
- 15% individual presentation and discussion of a research paper (second or third quarter);
- 30% final class project (individual or in groups up to two), evaluated through presentation, write-up document and software artifacts delivered (towards the end of the course).

This course counts as a depth course in theory for PhD students.

Viktor Kuncak is the instructor. Nicolas Voirol is the teaching assistant.

The closest to the textbook is Calculus of Computation (also available from Amazon)

We will make use of verification tools to verify programs and also learn how these tools work. One such tool in particular is Leon:

Please register on Moodle if you are interested in taking this course or send one of the instructors an email.

You can find the course schedule and room locations in the IC catalog course description.

See the 2013 version for a flavor of what to expect.

The course book contains some official learning outcomes:

- Formalize program correctness
- Prove correctness of programs on paper
- Sketch an automated verification algorithm
- Interpret results of verification systems
- Create a simple program verifier
- Construct a constraint solver
- Systematize approaches to software correctness
- Choose an appropriate technique for improving software reliability

EPFL professors are required to create such learning outcomes using a set of predefined phrases and verbs. To complement this, here are some **unofficial** learning outcomes and conclusions that should make sense after you take this course (selected by their humor content):

- The thing with weakest preconditions is that they are all backwards!
- In every class there is a person such that if they sleep, then everybody in this class sleeps. (First order logic neither implies nor rules out the possibility that this person is the course instructor.)
- All things being equal, the universe is a singleton.
- Making a new resolution every year always leads to saturation, after at most omega zero years.
- The meaning of life is the least fixed point of a monotonic transformer.
- Model checking can be exhaustive for finite state systems, which applies to fashion industry.
- A cheese sandwich is better than eternal happiness. Indeed: nothing is better than eternal happiness and a cheese sandwich is better than nothing. - I learned this important application of transitivity from this book, What is the name of this book?. Interestingly, the theory of transitive relations is expressible in effectively propositional logic, so satisfiability of ground formulas modulo this theory is decidable.

To follow this course, you need to know some discrete math. Some ideas about infinities come in handy in this course, though mostly we deal with countable sets, such as the set of reachable states of a program.