Location: Courses | CL Homepage | Dept. of Appl. Inf. (AI and DP) | Faculty of Math., Physics, and Inf. | Comenius Univ. Bratislava | Slovakia

1-AIN-470 Specification and Verification of Programs

News

Info

Here you will find the course information sheet.

Goal

The course develops students' ability to demonstrate the correctness of programs, formally specify the required properties and proving them using various methods, particularly structural induction. Graduates gain knowledge of a particular formalization of recursive programs, proving their properties within a single logical theory Peano arithmetic. They also get hands-on experience with the specification and verification of a large number of programs.

Syllabus

Declarative Programming. Primitive recursion. Recursion with measure. Iterative recursion. Recursion on notation. Pairing function and arithmetization. Structural recursion.

Specification-verification System. Peano Arithmetic. Mathematical induction. Extensions of arithmetic. Derived induction principles: complete induction, measure induction, structural induction.

Data Structures. Strings. Lists. Basic operations over lists. Sorting of lists. Applications of lists. Binary trees. Basic operations over binary trees. Binary search trees. Applications of trees. Symbolic expressions. Interpreter of programming language. Universal function.

Literature

Semesters

* – updated within last 7 days Last modified: 2024-03-01T15:30+0100