This class is taught (continuously) in Spring'08. The overall content is similar to previous year's class.

Official page in the course catalog, with course schedule

Lecturer: Viktor Kuncak

Teaching Assistant: Ruzica Piskac (Office Hours: every Tuesday, 16:00-18:00, BC343)

The material from the following bachelor EPFL courses is a prerequisites for this course:

• Discrete structures (CS-150)
• Algorithms (CS-250)
• Theoretical Computer Science (CS-251)
• Compiler Construction
• Advanced Theoretical Computer Science

The following master's courses are recommended and synergistic with this course:

• Advanced Compiler Construction (CS-420)
• Foundations of Software (CS-452)
• Model Checking (CS-552)
• Mathematical Logic II
• Advanced Computer Networks and Distributes Systems (CS-520)
• Principles of Dependable Systems (CS-521)
• Applications for Convex Optimization and Linear Programming (CS-453)

You can verify the content of these courses from the study program available online at school web site

The topics in the class will come from three cross-cutting themes of software analysis and verification:

• logic and automated reasoning (first order and higher order logic, decision procedures, first-order provers, interactive provers)
• reasoning about programs (relational semantics of programs, verification condition generation, abstract interpretation)
• systems and methodology (modular analysis and specification, constraint solving, bug finding, tool integration, examples of existing tools)

Lecture notes in the form of wiki should cover the material we present.

Calculus of Computation Textbook and the corresponding PiVC tool are the closest in spirit to our class.

Nielson, Nielson: Semantics with Applications, A Formal Introduction introduces semantics and its application in analysis. Recommended reading.

• the web site with
  • excellent slides
  • automated generator for program analyzers

Gallier Logic Book is a good theoretical foundation of logic (available online), some of whose sections will be useful. More discrete math online is in Gallier Discrete Math Book Draft.

An Introduction to Mathematical Logic and Type Theory Textbook contains a lot of relevant and important theorems, including the compactness theorems.

Logic for Mathematics and Computer Science Textbook has a very good treatment of equality in logic.

Some online resources for the class.

We will be using several verification tools, including

• Jahob system developed in our Laboratory for Automated Reasoning and Analysis
• PiVC tool which comes with the Calculus of Computation Textbook
• perhaps some others, see resources page
• you will build your own!

Installation

• you should be able to install those systems yourself
• we will do our best to provide working software in BC07
• we know how to install it for Linux

Official page in the course catalog, with course schedule

You must attend exercises: teaching assistant will verify the attendance, you need to attend 10/14 classes and you will need to present your homeworks in some of them

You should attend lectures: no one will verify your attendance, but grade is based in part on participating in class by asking and answering questions and writing selected answers in the wiki.

Homeworks will typically have a theoretical component and a programming part.

Programming part will be done in the Scala programming language developed in LAMP.

We will provide code skeletons. Using these skeletons and basic Scala documentation, the language should not present a problem.

Timing:

• weekly
• handed out on Thursday, due on Wednesday in 6 days

• Jointly with me formulate mini-project topic (as early as possible, but at latest by the middle of the semester)
• We will together design mini-project milestones (report on your project in later homeworks)
• Present a relevant scientific paper related to your project
• Final mini-project presentation at the end of the semester

• Final project write-up and presentation
• Homework write-up and presentation
• Paper presentation
• Scribing: completing the material in the Wiki and adding comments to reflect class discussion

Collaboration in groups 2-3 encouraged, but you must say who you collaborated with.

Homeworks

• at most 3 people for one homework
• everyone must be able to present all solutions in exercises (if you cannot present solution, you get negative points)

Projects

• at most 2 people for one project
• both must be familiar with all project details

• Most likely it will be neither the most difficult, nor the easiest EPFL course
• The course emphasizes independent work and will require substantial investment of time beyond lecture notes and exercises.
• It is designated as a master's course, but interested PhD students are encouraged to attend and can obtain credit for it.
• Do not take it just because of credits: should actually be interested in the material.