CS-550: Synthesis, Analysis, and Verification (SAV)


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.

Week 01 (Starting Monday 20.02.2017)

Week 02 (Starting Monday 27.02.2017)

Week 03 (Starting Monday 06.03.2017)

Week 04 (Starting Monday 13.03.2017)

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

Week 05 (Starting Monday 20.03.2017)

Week 06 (Starting Monday 27.03.2017)

Week 07 (Starting Monday 03.04.2017)

Week 08 (Starting Monday 10.04.2017)

Monday 14:15 INR 113 QUIZ
Monday 16:15 INR 113 QUIZ
Friday 13:15 INF 119 Holiday

Quizzes from previous years:


Week 09 (Starting Monday 24.04.2017)

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

Week 10 (Starting Monday 01.05.2017)

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

Week 11 (Starting Monday 08.05.2017)

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

Week 12 (Starting Monday 15.05.2017)

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

Week 13 (Starting Monday 22.05.2017)

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

Week 14 (Starting Monday 29.05.2017)

Monday 14:15 INR 113 Project Presentations
Friday 13:15 INF 119 Project Presentations

General Information

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.