FI:IV022 Design and Verification - Course Information
IV022 Design and verification of algorithms
Faculty of InformaticsSpring 2021
- Extent and Intensity
- 2/0. 2 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
- Teacher(s)
- prof. RNDr. Luboš Brim, CSc. (lecturer)
- Guaranteed by
- prof. RNDr. Luboš Brim, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Luboš Brim, CSc.
Supplier department: Department of Computer Science – Faculty of Informatics - Timetable
- Wed 10:00–11:50 Virtuální místnost
- Course Enrolment Limitations
- The course is also offered to the students of the fields other than those the course is directly associated with.
- fields of study / plans the course is directly associated with
- Image Processing and Analysis (programme FI, N-VIZ)
- Applied Informatics (programme FI, B-AP)
- Applied Informatics (programme FI, N-AP)
- Information Technology Security (eng.) (programme FI, N-IN)
- Information Technology Security (programme FI, N-IN)
- Bioinformatics and systems biology (programme FI, N-UIZD)
- Bioinformatics (programme FI, B-AP)
- Bioinformatics (programme FI, N-AP)
- Computer Games Development (programme FI, N-VIZ_A)
- Computer Graphics and Visualisation (programme FI, N-VIZ_A)
- Computer Networks and Communications (programme FI, N-PSKB_A)
- Cybersecurity Management (programme FI, N-RSSS_A)
- Formal analysis of computer systems (programme FI, N-TEI)
- Graphic design (programme FI, N-VIZ)
- Graphic Design (programme FI, N-VIZ_A)
- Hardware Systems (programme FI, N-PSKB_A)
- Hardware systems (programme FI, N-PSKB)
- Image Processing and Analysis (programme FI, N-VIZ_A)
- Information security (programme FI, N-PSKB)
- Information Systems (programme FI, N-IN)
- 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 (eng.) (programme FI, D-IN4)
- Informatics (programme FI, B-INF) (2)
- Informatics (programme FI, D-IN4)
- Informatics in education (programme FI, B-IVV) (2)
- Information Security (programme FI, N-PSKB_A)
- Quantum and Other Nonclassical Computational Models (programme FI, N-TEI)
- 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 visualisation (programme FI, N-VIZ)
- 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 Networks and Communications (programme FI, N-PSKB)
- Computer Systems and Technologies (eng.) (programme FI, D-IN4)
- Computer Systems and Technologies (programme FI, D-IN4)
- Computer Systems and Data Processing (programme FI, B-IN)
- Computer Systems (programme FI, N-IN)
- Principles of programming languages (programme FI, N-TEI)
- Programming and development (programme FI, B-PVA)
- Embedded Systems (eng.) (programme FI, N-IN)
- Programmable Technical Structures (programme FI, B-IN)
- Embedded Systems (programme FI, N-IN)
- Cybersecurity management (programme FI, N-RSSS)
- Services development management (programme FI, N-RSSS)
- Software Systems Development Management (programme FI, N-RSSS)
- Services Development Management (programme FI, N-RSSS_A)
- 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)
- Software Systems Development Management (programme FI, N-RSSS_A)
- Software Systems (programme FI, N-PSKB_A)
- Software systems (programme FI, N-PSKB)
- Machine learning and artificial intelligence (programme FI, N-UIZD)
- Theoretical Informatics (programme FI, N-IN)
- Teacher of Informatics and IT administrator (programme FI, N-UCI)
- Informatics for secondary school teachers (programme FI, N-UCI) (2)
- 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)
- Computer Games Development (programme FI, N-VIZ)
- Processing and analysis of large-scale data (programme FI, N-UIZD)
- Image Processing (programme FI, N-AP)
- Natural language processing (programme FI, N-UIZD)
- Course objectives
- The goal is to get acquaint with methods for design and verification of small sequential algorithms. The students acquire basic verification techniques.
- Learning outcomes
- By the end of the semester, students should be able to develop small sequential algorithms and prove their correctness.
- Syllabus
- Programs as predicate transformers, weakest precondition, properties of predicate transformers, program correctness.
- Garded command language. Skip and abort commands, composition, alternative command, iterative command.
- Verification of programs, proof outlines, verification rules for sequential composition, alternative, and loop commands. Array manipulation.
- Constructive verification of programs, basic principles and strategies, developing loops from invariants and bounds, developing invarinats.
- Examples of program development. Deriving of efficient algorithms, Searching and sorting.
- Literature
- DIJKSTRA, Edsger W. and W. H. J. FEIJEN. A method of programming. Wokingham: Addison-Wesley Publishing Company, 1998, vii, 188 s. ISBN 0-201-17536-3. info
- KALDEWAIJ, A. Programming :the derivation of algorithms. New York: Prentice Hall, 1990, xii, 216 s. ISBN 0-13-204108-1. info
- GRIES, David. The Science of Programming. New York: Springer-Verlag, 1981, 366 s., ob. ISBN 0-387-90641-X. info
- Teaching methods
- lecture, homeworks, reading
- Assessment methods
- Final exam is written. In the case homeworks are assigned, these are counted by maximum of 30% to the final mark. No study materials are allowed during the final examination.
- Language of instruction
- Czech
- Further Comments
- The course is taught annually.
- Teacher's information
- https://www.fi.muni.cz/usr/brim/home/#teaching
- Enrolment Statistics (Spring 2021, recent)
- Permalink: https://is.muni.cz/course/fi/spring2021/IV022