Program Semantics - NSWI183

• Title: Sémantika programů
• Form of teaching: seminar
• Guaranteed by: Department of Distributed and Dependable Systems (32-KDSS)
• Faculty: Faculty of Mathematics and Physics
• Actual: from 2024
• Duration in semesters: 1
• Semester: winter
• E-Credits: 3
• Hours per week, examination: winter s.:0/2, C [HT]
• Capacity: unlimited
• Maximum number of enrolled students: unlimited
• Min. number of students: unlimited
• 4EU+: no
• Virtual mobility / capacity: no
• State of the course: taught
• Language: Czech
• Teaching methods: full-time
• Repeated enrollment: 2 / 2 / 2 / 2
• Guarantor: doc. RNDr. Jan Kofroň, Ph.D.
• Teacher(s): doc. RNDr. Jan Kofroň, Ph.D.
• Class: Informatika Bc.
• Classification: Informatics > Software Engineering
• Interchangeability : NSWI162
• Is interchangeable with: NSWI162

Annotation

English

The aim of the course is to introduce students to the basics of the semantics of imperative programming languages. Students will be introduced to the tool for verification of the properties of PiVC programs. The second half of the course will be devoted to the Dafny tools for verification of real programs against specifications written in the form of annotations directly in the program. Credit will be awarded for Work on three to five smaller-scale homework.

Last update: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)

Czech

Cílem kurzu je seznámit studenty se základy sémantiky imperativních programovacích jazyků. Studenti budou seznámeni s nástrojem pro verifikaci vlastností programů PiVC. Druhá polovina kurzu bude věnována nástroji Dafny pro verifikaci reálných programů proti specifikacím zapsaným v podobě anotací přímo v programu. Zápočet bude udělen za vypracování tří až pěti domácích úloh menšího rozsahu.

Last update: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)

Literature

English

A. R. Bradley, Z. Manna: The Calculus of Computation, Springer-Verlag, 2007

E. M. Clarke, O. Grumberg, D. A. Peled: Model Checking, MIT Press, 1999

The Dafny Programming and Verification Language – https://dafny.org/

Last update: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)

Syllabus

English

1) Introduction to the concept of program semantics

2) Methods of specification of properties of imperative programs

3) Mathematical foundations of specification

4) Proving the properties of programs

5) Dafny verification tool

Last update: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)

Czech

1) Predstavení pojmu sémantiky programu

2) Metody specifikace vlastností imperativních programu

3) Matematické základy specifikace

4) Dokazování vlastností programu

5) Verifikacní nástroj Dafny

Last update: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)