Page in Course Catalog and pdf version

This class is taught in Spring'09. The overall content is similar to Software Analysis and Verification 2008 with some changes from 2008.

Schedule:

• Wednesday 11:15-12:45 in BC01
• Thursday 14:15-16:00 in BC01

Teaching staff:

• Viktor Kuncak (lecturer)
• Ruzica Piskac (PhD assistant)
• Philippe Suter (PhD assistant)
• Sebastian Gfeller (MSc assistant)
• Danielle Chamberlain (course secretary)

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:

• reasoning about programs (relational semantics of programs, verification condition generation, abstract interpretation)
• logic and automated reasoning (first order and higher order logic, decision procedures, first-order provers, interactive provers)
• 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 most of 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
  • 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 may 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

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.

• if you do not know Scala, try to work in a group with someone who knows

Homework timing:

• weekly or bi-weekly
• we hand out assignments on Thursday, your solutions are due Thursday before 14:00

• Jointly with me formulate mini-project topic (as early as possible, 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
• Course participation

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: you should actually be interested in the material.