FI:IV101 Seminar on verification - Course Information

IV101 Seminar on verification

Extent and Intensity

0/2. 2 credit(s). Type of Completion: z (credit).

Teacher(s)

prof. RNDr. Jiří Barnat, Ph.D. (lecturer)

Guaranteed by

prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics

Timetable

Mon 12:00–13:50 C408

Course Enrolment Limitations

The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 12 student(s).
Current registration and enrolment status: enrolled: 0/12, only registered: 0/12, only registered with preference (fields directly associated with the programme): 0/12

fields of study / plans the course is directly associated with

• Applied Informatics (programme FI, B-AP)
• Applied Informatics (programme FI, N-AP)
• Information Technology Security (programme FI, N-IN)
• Bioinformatics (programme FI, B-AP)
• Bioinformatics (programme FI, N-AP)
• Information Systems (programme FI, N-IN)
• Informatics with another discipline (programme FI, B-BI)
• Informatics with another discipline (programme FI, B-EB)
• Informatics with another discipline (programme FI, B-FY)
• Informatics with another discipline (programme FI, B-GE)
• Informatics with another discipline (programme FI, B-GK)
• Informatics with another discipline (programme FI, B-CH)
• Informatics with another discipline (programme FI, B-IO)
• Informatics with another discipline (programme FI, B-MA)
• Informatics with another discipline (programme FI, B-TV)
• Informatics (programme FI, N-IN)
• Mathematical Informatics (programme FI, B-IN)
• Parallel and Distributed Systems (programme FI, B-IN)
• Parallel and Distributed Systems (programme FI, N-IN)
• Computer Graphics and Image Processing (programme FI, B-IN)
• Computer Graphics (programme FI, N-IN)
• Computer Networks and Communication (programme FI, B-IN)
• Computer Networks and Communication (programme FI, N-IN)
• Computer Systems and Data Processing (programme FI, B-IN)
• Computer Systems (programme FI, N-IN)
• Embedded Systems (eng.) (programme FI, N-IN)
• Programmable Technical Structures (programme FI, B-IN)
• Embedded Systems (programme FI, N-IN)
• Service Science, Management and Engineering (eng.) (programme FI, N-AP)
• Service Science, Management and Engineering (programme FI, N-AP)
• Social Informatics (programme FI, B-AP)
• Theoretical Informatics (programme FI, N-IN)
• Upper Secondary School Teacher Training in Informatics (programme FI, N-SS) (2)
• Artificial Intelligence and Natural Language Processing (programme FI, B-IN)
• Artificial Intelligence and Natural Language Processing (programme FI, N-IN)
• Image Processing (programme FI, N-AP)

Course objectives

At the end of the course, students will have practical experience with automated verification of computer systems. They will be able to use most standard model checkers, such as DiVinE, SPIN, UPPAAL, PRISM, etc.

Syllabus

• In the seminar the students get introduced to several verification tools, formal languages for describing typical properties of systems, and they will work on a student project.

Literature

• Peled, Doron. Software Reliability Methods. Springer, 2001.
• HOLZMANN, Gerald J. The spin model checker :primer and reference manual. Boston: Addison-Wesley, 2004, xii, 596 s. ISBN 0-321-22862-6. info
• GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info

Teaching methods

lectures, group projects

Assessment methods

Students are evaluated according their individual work on the project.

Language of instruction

Czech

Further Comments

Study Materials
The course is taught once in two years.

Teacher's information

http://www.fi.muni.cz/~xbarnat/IV101/

• Enrolment Statistics (Spring 2012, recent)
  
• Permalink: https://is.muni.cz/course/fi/spring2012/IV101