IV101 Seminar on verification

Faculty of Informatics
Spring 2015
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 16:00–17:50 C416
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
there are 35 fields of study the course is directly associated with, display
Course objectives
At the end of the course, students will have practical experience with automated verification of computer systems. Within the seminar students will get introduced to a couple of verification tools, and formalisms to express program properties. Students have to prepare and give a presentation to other participants of the seminar describing a selected verification tool. Expected length of the presentation is about an hour and half.
Syllabus
  • In the seminar the students get introduced to several verification tools, formal languages for describing typical properties of systems, and they will prepare a presentation on selected verification tool.
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 lead by students, preparation of own presentation, presentation
Assessment methods
Students are evaluated according their individual work on the presentation.
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/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013.

IV101 Seminar on verification

Faculty of Informatics
Spring 2013
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 13:00–14:50 B411
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
there are 37 fields of study the course is directly associated with, display
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/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2012
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
there are 37 fields of study the course is directly associated with, display
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/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2010
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
Timetable
Mon 12:00–13:50 B411
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
there are 36 fields of study the course is directly associated with, display
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 annually.
Teacher's information
http://www.fi.muni.cz/~xbarnat/IV101/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2009
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
Timetable
Mon 12:00–13:50 B411
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
there are 33 fields of study the course is directly associated with, display
Course objectives
In this seminar students will acquire practical experience with automated verification of computer systems. In particular, they will be able use most of the standard model checkers, such as 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 practical 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
Assessment methods
Students are evaluated according their individual work on the project.
Language of instruction
Czech
Further Comments
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~xbarnat/IV101/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2008
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
Prerequisites (in Czech)
SOUHLAS
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
there are 37 fields of study the course is directly associated with, display
Course objectives
The goal is to acquire practical experience in automated verification of parallel and distributed systems.
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 practical 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
Assessment methods (in Czech)
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Language of instruction
Czech
Further Comments
The course is taught annually.
The course is taught: every week.
Teacher's information
http://www.fi.muni.cz/~xbarnat/IV101/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2007
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
Timetable
Mon 14:00–15:50 B411
Prerequisites (in Czech)
SOUHLAS
Course Enrolment Limitations
The course is only offered to the students of the study fields 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
fields of study / plans the course is directly associated with
there are 17 fields of study the course is directly associated with, display
Course objectives
The goal is to acquire practical experience in automated verification of parallel and distributed systems.
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 practical 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
Assessment methods (in Czech)
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Language of instruction
Czech
Further Comments
The course is taught annually.
Teacher's information
http://www.fi.muni.cz/~xbarnat/IV101/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Autumn 2005
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
Timetable
Wed 8:00–9:50 B411
Prerequisites (in Czech)
SOUHLAS
Course Enrolment Limitations
The course is only offered to the students of the study fields 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
fields of study / plans the course is directly associated with
there are 17 fields of study the course is directly associated with, display
Course objectives
The goal is to acquire practical experience in automated verification of parallel and distributed systems.
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 practical project. The seminar supplements the courses "Communication and Parallelism" and "Parallel and Distributed Systems".
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
Assessment methods (in Czech)
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Language of instruction
Czech
Further Comments
The course is taught each semester.
Teacher's information
http://www.fi.muni.cz/usr/brim/IV101
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2005
Extent and Intensity
0/2. 2 credit(s). Type of Completion: z (credit).
Teacher(s)
prof. RNDr. Luboš Brim, CSc. (lecturer), prof. RNDr. Jiří Barnat, Ph.D. (deputy)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Prerequisites (in Czech)
SOUHLAS
Course Enrolment Limitations
The course is only offered to the students of the study fields 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
fields of study / plans the course is directly associated with
there are 17 fields of study the course is directly associated with, display
Course objectives
The goal is to acquire practical experience in automated verification of parallel and distributed systems.
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 practical project. The seminar supplements the courses "Communication and Parallelism" and "Parallel and Distributed Systems".
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
Assessment methods (in Czech)
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Language of instruction
Czech
Further Comments
The course is taught each semester.
The course is taught: every week.
Teacher's information
http://www.fi.muni.cz/usr/brim/IV101
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Autumn 2004
Extent and Intensity
0/2. 2 credit(s). Type of Completion: z (credit).
Teacher(s)
prof. RNDr. Jiří Barnat, Ph.D. (lecturer)
prof. RNDr. Luboš Brim, CSc. (lecturer)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Timetable
each odd Thursday 14:00–17:50 B003
Prerequisites (in Czech)
SOUHLAS
Course Enrolment Limitations
The course is only offered to the students of the study fields 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
fields of study / plans the course is directly associated with
there are 17 fields of study the course is directly associated with, display
Course objectives
The goal is to acquire practical experience in automated verification of parallel and distributed systems.
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 practical project. The seminar supplements the courses "Communication and Parallelism" and "Parallel and Distributed Systems".
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
Assessment methods (in Czech)
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Language of instruction
Czech
Further Comments
The course is taught each semester.
Teacher's information
http://www.fi.muni.cz/usr/brim/IV101
The course is also listed under the following terms Autumn 2003, Spring 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2004
Extent and Intensity
0/2. 2 credit(s). Type of Completion: z (credit).
Teacher(s)
prof. RNDr. Luboš Brim, CSc. (lecturer)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Prerequisites (in Czech)
SOUHLAS
Course Enrolment Limitations
The course is only offered to the students of the study fields 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
fields of study / plans the course is directly associated with
Course objectives (in Czech)
Cílem semináře je získání praktických dovedností a zkušeností s automatizovanou verifikací zejména paralelních a distribuovaných systémů.
Syllabus (in Czech)
  • V rámci semináře se studenti seznámí s několika nejpoužívanějšími verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systémů a vypracují verifikační projekt v rozsahu 15 hod. Seminář doplňuje předměty "Komunikace a paralelismus" a "Paralelní a distribuované výpočty".
Literature
  • Peled, Doron. Software Reliability Methods. Springer, 2001.
  • GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Assessment methods (in Czech)
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Language of instruction
Czech
Further Comments
The course is taught each semester.
The course is taught: every week.
Teacher's information
http://www.fi.muni.cz/usr/brim/IV101
The course is also listed under the following terms Autumn 2003, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Autumn 2003
Extent and Intensity
0/2. 2 credit(s). Type of Completion: z (credit).
Teacher(s)
prof. RNDr. Luboš Brim, CSc. (lecturer)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Prerequisites (in Czech)
SOUHLAS
Course Enrolment Limitations
The course is only offered to the students of the study fields 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
fields of study / plans the course is directly associated with
Course objectives (in Czech)
Cílem semináře je získání praktických dovedností a zkušeností s automatizovanou verifikací zejména paralelních a distribuovaných systémů.
Syllabus (in Czech)
  • V rámci semináře se studenti seznámí s několika nejpoužívanějšími verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systémů a vypracují verifikační projekt v rozsahu 15 hod. Seminář doplňuje předměty "Komunikace a paralelismus" a "Paralelní a distribuované výpočty".
Literature
  • Peled, Doron. Software Reliability Methods. Springer, 2001.
  • GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Assessment methods (in Czech)
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Language of instruction
Czech
Further Comments
The course is taught each semester.
The course is taught: every week.
Teacher's information
http://www.fi.muni.cz/usr/brim/IV101
The course is also listed under the following terms Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2019

The course is not taught in Spring 2019

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
Prerequisites (in Czech)
IV113 Validation and Verification
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
there are 36 fields of study the course is directly associated with, display
Course objectives
At the end of the course, students will have practical experience with automated verification of computer systems. Within the seminar students will get introduced to a couple of verification tools, and formalisms to express program properties. Students have to prepare and give a presentation to other participants of the seminar describing a selected verification tool. Expected length of the presentation is about an hour and half.
Syllabus
  • In the seminar the students get introduced to several verification tools, formal languages for describing typical properties of systems, and they will prepare a presentation on selected verification tool.
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 lead by students, preparation of own presentation, presentation
Assessment methods
Students are evaluated according their individual work on the presentation.
Language of instruction
Czech
Further Comments
The course is taught annually.
The course is taught: every week.
Teacher's information
http://www.fi.muni.cz/~xbarnat/IV101/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2018

The course is not taught in Spring 2018

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
Prerequisites (in Czech)
IV113 Validation and Verification
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
there are 36 fields of study the course is directly associated with, display
Course objectives
At the end of the course, students will have practical experience with automated verification of computer systems. Within the seminar students will get introduced to a couple of verification tools, and formalisms to express program properties. Students have to prepare and give a presentation to other participants of the seminar describing a selected verification tool. Expected length of the presentation is about an hour and half.
Syllabus
  • In the seminar the students get introduced to several verification tools, formal languages for describing typical properties of systems, and they will prepare a presentation on selected verification tool.
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 lead by students, preparation of own presentation, presentation
Assessment methods
Students are evaluated according their individual work on the presentation.
Language of instruction
Czech
Further Comments
The course is taught annually.
The course is taught: every week.
Teacher's information
http://www.fi.muni.cz/~xbarnat/IV101/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2017

The course is not taught in Spring 2017

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
Prerequisites (in Czech)
IV113 Validation and Verification
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
there are 36 fields of study the course is directly associated with, display
Course objectives
At the end of the course, students will have practical experience with automated verification of computer systems. Within the seminar students will get introduced to a couple of verification tools, and formalisms to express program properties. Students have to prepare and give a presentation to other participants of the seminar describing a selected verification tool. Expected length of the presentation is about an hour and half.
Syllabus
  • In the seminar the students get introduced to several verification tools, formal languages for describing typical properties of systems, and they will prepare a presentation on selected verification tool.
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 lead by students, preparation of own presentation, presentation
Assessment methods
Students are evaluated according their individual work on the presentation.
Language of instruction
Czech
Further Comments
The course is taught annually.
The course is taught: every week.
Teacher's information
http://www.fi.muni.cz/~xbarnat/IV101/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2016

The course is not taught in Spring 2016

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
Prerequisites (in Czech)
IV113 Validation and Verification
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
there are 36 fields of study the course is directly associated with, display
Course objectives
At the end of the course, students will have practical experience with automated verification of computer systems. Within the seminar students will get introduced to a couple of verification tools, and formalisms to express program properties. Students have to prepare and give a presentation to other participants of the seminar describing a selected verification tool. Expected length of the presentation is about an hour and half.
Syllabus
  • In the seminar the students get introduced to several verification tools, formal languages for describing typical properties of systems, and they will prepare a presentation on selected verification tool.
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 lead by students, preparation of own presentation, presentation
Assessment methods
Students are evaluated according their individual work on the presentation.
Language of instruction
Czech
Further Comments
The course is taught annually.
The course is taught: every week.
Teacher's information
http://www.fi.muni.cz/~xbarnat/IV101/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2014

The course is not taught in Spring 2014

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
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
there are 35 fields of study the course is directly associated with, display
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
The course is taught once in two years.
The course is taught: every week.
Teacher's information
http://www.fi.muni.cz/~xbarnat/IV101/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2011

The course is not taught in Spring 2011

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
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
there are 36 fields of study the course is directly associated with, display
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
The course is taught once in two years.
The course is taught: every week.
Teacher's information
http://www.fi.muni.cz/~xbarnat/IV101/
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Spring 2003

The course is not taught in Spring 2003

Extent and Intensity
0/2. 2 credit(s) (plus extra credits for completion). Type of Completion: z (credit).
Teacher(s)
prof. RNDr. Luboš Brim, CSc. (lecturer)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Course Enrolment Limitations
The course is only offered to the students of the study fields the course is directly associated with.

The capacity limit for the course is 20 student(s).
Current registration and enrolment status: enrolled: 0/20, only registered: 0/20
fields of study / plans the course is directly associated with
Course objectives (in Czech)
Cílem semináře je získání praktických dovedností a zkušeností s automatizovanou verifikací zejména paralelních a distribuovaných systémů.
Syllabus (in Czech)
  • V rámci semináře se studenti seznámí s několika nejpoužívanějšími verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systémů a vypracují verifikační projekt v rozsahu 15 hod. Seminář doplňuje předměty "Komunikace a paralelismus" a "Paralelní a distribuované výpočty".
Literature
  • Peled, Doron. Software Reliability Methods. Springer, 2001.
  • GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Language of instruction
Czech
Further Comments
The course is taught each semester.
The course is taught: every week.
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.

IV101 Seminar on verification

Faculty of Informatics
Autumn 2002

The course is not taught in Autumn 2002

Extent and Intensity
0/2. 2 credit(s) (plus extra credits for completion). Type of Completion: z (credit).
Teacher(s)
prof. RNDr. Luboš Brim, CSc. (lecturer)
Guaranteed by
prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Course Enrolment Limitations
The course is only offered to the students of the study fields the course is directly associated with.

The capacity limit for the course is 20 student(s).
Current registration and enrolment status: enrolled: 0/20, only registered: 0/20
fields of study / plans the course is directly associated with
Course objectives (in Czech)
Cílem semináře je získání praktických dovedností a zkušeností s automatizovanou verifikací zejména paralelních a distribuovaných systémů.
Syllabus (in Czech)
  • V rámci semináře se studenti seznámí s několika nejpoužívanějšími verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systémů a vypracují verifikační projekt v rozsahu 15 hod. Seminář doplňuje předměty "Komunikace a paralelismus" a "Paralelní a distribuované výpočty".
Literature
  • Peled, Doron. Software Reliability Methods. Springer, 2001.
  • GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Language of instruction
Czech
Further Comments
The course is taught each semester.
The course is taught: every week.
The course is also listed under the following terms Autumn 2003, Spring 2004, Autumn 2004, Spring 2005, Autumn 2005, Spring 2007, Spring 2008, Spring 2009, Spring 2010, Spring 2012, Spring 2013, Spring 2015.
  • Enrolment Statistics (recent)