Subjects

Your browser does not support JavaScript, or its support is disabled. Some features may not be available.

Program Semantics - NSWI183

Title:	Sémantika programů
Guaranteed by:	Department of Distributed and Dependable Systems (32-KDSS)
Faculty:	Faculty of Mathematics and Physics
Actual:	from 2024
Semester:	winter
E-Credits:	3
Hours per week, examination:	winter s.:0/2, C [HT]
Capacity:	unlimited
Min. number of students:	unlimited
4EU+:	no
Virtual mobility / capacity:	no
State of the course:	taught
Language:	Czech
Teaching methods:	full-time

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

Opinion survey results Examination dates WS schedule Noticeboard

Annotation -

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)

Literature -

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 -

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)