- Wednesday 11:15-12:45 in BC01
- Thursday 14:15-16:00 in BC01
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:
- 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.
Nielson, Nielson: Semantics with Applications, A Formal Introduction introduces semantics and its application in analysis. Recommended reading.
- the web site with
- 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 may 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
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.
- if you do not know Scala, try to work in a group with someone who knows
- 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
What Determines Your Grade
- 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.
- 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: you should actually be interested in the material.