Search programme

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

​​​

Syllabus for

Academic year
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)
TITEA SOFTWARE ENGINEERING, Year 4 (elective)
TITEA SOFTWARE ENGINEERING, Year 3 (elective)
TDATA COMPUTER SCIENCE AND ENGINEERING - Computer Languages, Year 4 (elective)
TDATA COMPUTER SCIENCE AND ENGINEERING - Engineering of Computer-Based Systems, Year 4 (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.


Page manager Published: Thu 03 Nov 2022.