Software Analysis and Verification 2008 (SAV'08)
This class is taught (continuously) in Spring'08. The overall content is similar to previous year's class.
Lecturer: Viktor Kuncak
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)
- 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.
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
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
- perhaps some others, see resources page
- you will build your own!
- 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
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.
We will provide code skeletons. Using these skeletons and basic Scala documentation, the language should not present a problem.
- 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
What Determines Your Grade
- 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.
- 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)
- at most 2 people for one project
- both must be familiar with all project details
Is This Course Difficult?
- 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.