|
Learning goals: to become familiar with, and acquire insight on the underlying concepts of:
- program semantics: operational, denotational, axiomatic.
- formalisms to express programs' correctness: Hoare-style, LTL, CTL, , CSP.
- automated verification techniques: predicate transformation/symbolic execution, automated theorem proving, model checking (LTL,, CTL, symbolic), refinement checking.
Additionally, to acquire hands-on experience with :
- implementing and optimizing a verification technique.
- using a verification tool to model a problem and conduct a verification of its solution.
Assessment
In principle 15% assignments, 40% projects, 45% exams. This distribution can be changed depending on the composition of the projects, but in any case the exam form and grading will be announced and fixed at the start of the course.
To pass the course the average of the tests should be at least 5.0.
To qualify for a repair test, the grade of the original must be at least a 4.
The retake can replace one of the tests. So, the coverage of the retake is the same as the coverage of the test it replaces.
Prerequisites
Background in predicate logic, experience with a functional programming language, e.g. Haskell or ML.
|
 |
|
Most modern software is quite complex.
The most widely used approach to verify them is still by testing, which is inherently incomplete and hard to scale up to cover the complexity.
In this course we will discuss a number of advanced validation and verification techniques that go far beyond ad-hoc testing.
Exploiting them is an important key towards more reliable complex software.
We will in particular focus on techniques that can be automated, or at least partially automated:
- Predicate transformation technique, which you can use to symbolically execute a program to calculate its range of input or output. This leads to the bounded but symbolic and fully automated verification technique.
- Common automated theorem proving techniques, used as the back-end of symbolic execution based verification.
- We will also discuss several common ways to define the semantic of programs, from which correctness can be defined and proven.
- Model checking techniques, that can be used to either fully verify a model of a program, even if the number of possible executions is infinite, or to boundedly verify the program itself.
Course form
Lectures, projects.
Literature
Lecture notes, on-line documentation, and papers.
|
|
|