Sémantika programů - NSWI183

• Anglický název: Program Semantics
• Zajišťuje: Katedra distribuovaných a spolehlivých systémů (32-KDSS)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2024
• Semestr: zimní
• E-Kredity: 3
• Rozsah, examinace: zimní s.:0/2, Z [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: čeština
• Způsob výuky: prezenční
• Garant: doc. RNDr. Jan Kofroň, Ph.D.
• Vyučující: doc. RNDr. Jan Kofroň, Ph.D.
• Třída: Informatika Bc.
• Kategorizace předmětu: Informatika > Softwarové inženýrství
• Záměnnost : NSWI162
• Je záměnnost pro: NSWI162

Anotace

čeština

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.

Poslední úprava: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)

angličtina

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.

Poslední úprava: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)

Literatura

čeština

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/

Poslední úprava: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)

Sylabus

čeština

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

Poslední úprava: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)

angličtina

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

Poslední úprava: Hnětynka Petr, doc. RNDr., Ph.D. (24.04.2024)