Search programme

​Use the search function to search amongst programmes at Chalmers. The study programme and the study programme syllabus relating to your studies are generally from the academic year you began your studies.

Syllabus for

Academic year
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.


Page manager Published: Mon 28 Nov 2016.