LARA

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.

Quizzes from previous years:

• 2015 Solutions
• 2013 Solutions

Paper 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:

http://leon.epfl.ch/

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.