Syllabus for |
|
| TDA565 - Program verification |
| |
| Owner: TITEA |
|
|
5,0 Credits (ECTS 7,5) |
| Grading: TH - Five, Four, Three, Not passed |
| Level: B |
|
Department: 37 - COMPUTER SCIENCE AND ENGINEERING
|
Teaching language: English
| Course module |
|
Credit distribution |
|
Examination dates |
|
Sp1 |
Sp2 |
Sp3 |
Sp4 |
|
No Sp |
| 0104 |
Examination |
5,0 c |
Grading: TH |
|
|
5,0 c
|
|
|
|
|
|
Contact examiner 
|
| 0204 |
Laboratory |
0,0 c |
Grading: UG |
|
|
0,0 c
|
|
|
|
|
|
|
In programs
DCMAS MSc PROGR IN DEPENDABLE COMPUTER SYSTEMS, Year 1 (elective)
TDATA COMPUTER SCIENCE AND ENGINEERING - Computer Languages, Year 4 (elective)
TDATA COMPUTER SCIENCE AND ENGINEERING - Engineering of Computer-Based Systems, Year 4 (elective)
TITEA SOFTWARE ENGINEERING, Year 4 (elective)
TITEA SOFTWARE ENGINEERING, Year 3 (elective)
Examiner:
Univ lektor Catarina Coquand
Bitr professor
Koen Claessen
Eligibility:
For single subject courses within Chalmers programmes the same eligibility requirements apply, as to the programme(s) that the course is part of.
Course specific prerequisites
Data structures, functional programming, object-oriented programming, and logic (discrete mathematics year 1).
Aim
Program verification is about how to convince oneself that a program unit really does what it should. There are two dual methods for verifying programs that will be covered in this course: testing (which has the purpose of finding errors in a program in a systematic way), and proving (reasoning about the program in order to guarantee correctness). Verifying programs only makes sense if we have some kind of specification of what the program is supposed to do. Many specifications are written in natural language which might lead to impreciseness and misunderstandings. In the course we will describe how to use concrete precise methods for writing functional requirements. Such a precise specification will then be our base for the verification of programs. The course will discuss verification techniques both for imperative and functional programs.
Goal
After a completed course the student should know
- different techniques for writing precise specification of functional requirement of software units,
- how to systematically search for errors in an implementation (by testing) and measure how good the search is,
- how to reason about programs for guaranteeing correctness.
Content
Design-by-contract. Specifications: pre- and post-conditions, algebraic specification. Testing: priciples for test methods, random testing, coverage analysis. Verification: Hoare logic, equational reasoning.
Organisation
Lectures, exercise classes, and hand-ins.
Literature
See the homepage of the course.
Examination
Written exam.