LARA

Course Information: Synthesis, Analysis, and Verification 2010

Teaching Staff

This class is taught in Spring 2010. The overall content is similar to past courses:

Teaching staff:

Schedule:

  • Monday: 14:15-16:00 in INR 219 (usually lectures, usually by Viktor Kuncak)
  • Tuesday: 16:15-18:00 in INM 10 (usually blackboard exercises, usually by Ruzica Piskac)
  • Friday: 10:15-12:00 in INR 219 (exercises or programming labs, usually by Hossein Hojjatt)

Topics

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)

Useful Background Courses

The material from the following bachelor EPFL courses is directly useful for this course:

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

A relevant introductory PhD course: Theory of Computation (offered this semester by Prof. Bernard Moret)

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

General Reading Material and Textbooks

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

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.

Systems

We may be using several verification tools, including

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

What Determines Your Grade

  • Final project write-up and presentation
  • Homework (written and programmed)
  • Quizzes
  • Course participation

Projects

  • 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

Homeworks

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

  • goal is to understand the material and prepare for project

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 Tuesday, your solutions are due Tuesday before 16:00

Quizzes

We will have 45-minute long quizzes during lectures, exercises, or projects, to check the understanding of the material previously assigned in homeworks.

We will not announce quizzes too much in advance, so please make sure you understand what was covered so far in the course, and ask us immediately if something is unclear.

The quizzes will not carry as much weight as homeworks, but the results on quizzes can change your grade.

Collaboration Policy

Collaboration in groups of 2 is encouraged, but:

  • you must say who you collaborated with (we treat any 'unreported collaboration' as cheating!)
  • you must be able to explain your entire solution on the board if we ask you
  • there is no collaboration on quizzes!

Course Participation

Attend courses, exercises, labs, and answer questions

If you do not show up for a quiz, you get 0 points on that quiz.

Is This Course Difficult?

  • Most likely it will be neither the most difficult, nor the easiest EPFL course
  • We usually have several students that get each of 6, 5.5, 5, 4 (and a student who occasionally gives up and drops the course)
  • The course emphasizes independent work and will require substantial investment of time beyond lecture notes and exercises
  • It is formally 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
  • if we go too fast in the course, let us know - it may be due to our cruise control

What's the name of the course?

  • Q: Is this course still about Software Analysis and Verification?
  • A: Software, what else?

This year we may incorporate, for the first, time, some elements of automated synthesis: automatically constructing software fragments that meet the given specification. We will therefore informally use the broader course name Synthesis, Analysis, and Verification. (The name for the purpose of EPFL administration remains the same.)