Syllabus for |
|
| TDA565 - Program verification |
| |
| Owner: TKITE |
|
|
7,5 Credits |
| Grading: TH - Five, Four, Three, Not passed |
| Education cycle: First-cycle |
|
Major subject: Information Technology
|
|
Department: 37 - COMPUTER SCIENCE AND ENGINEERING
|
Teaching language: English
| Course module |
|
Credit distribution |
|
Examination dates |
|
Sp1 |
Sp2 |
Sp3 |
Sp4 |
|
No Sp |
| 0104 |
Examination |
7,5 c |
Grading: TH |
|
|
7,5 c
|
|
|
|
|
|
15 Dec 2007 am V, |
27 Mar 2008 pm V |
| 0204 |
Laboratory |
0,0 c |
Grading: UG |
|
|
0,0 c
|
|
|
|
|
|
|
In programs
TKDAT COMPUTER SCIENCE AND ENGINEERING, Year 3 (elective)
TKITE SOFTWARE ENGINEERING, Year 3
Examiner:
Univ lektor Catarina Coquand
Professor
Reiner Hähnle
Bitr professor
Patrik Jansson
Course evaluation:
http://document.chalmers.se/doc/1810829629
Go to Course Homepage
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
Object-oriented programming, data structures, 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.
Learning outcomes (after completion of the course the student should be able to)
* 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 and labs/hand-ins.