#
FI:DFOME Formal Methods - Course Information

## DFOME Formal Methods in Theory and Practice

**Faculty of Informatics**

Spring 2011

**Extent and Intensity**- 3/0. 3 credit(s). Type of Completion: z (credit).
**Teacher(s)**- prof. RNDr. Luboš Brim, CSc. (lecturer)

prof. RNDr. Ivana Černá, CSc. (lecturer)

prof. RNDr. Petr Hliněný, Ph.D. (lecturer)

prof. RNDr. Mojmír Křetínský, CSc. (lecturer)

prof. RNDr. Antonín Kučera, Ph.D. (lecturer)

Ing. Matej Lexa, Ph.D. (lecturer) **Guaranteed by**- prof. RNDr. Antonín Kučera, Ph.D.

Faculty of Informatics **Course Enrolment Limitations**- The course is only offered to the students of the study fields the course is directly associated with.

**Fields of study the course is directly associated with**- there are 8 fields of study the course is directly associated with, display
**Course objectives**- The course consists of several and relatively independent parts devoted to selected topics in formal methods. Each part starts with an introduction presented by a lecturer followed by students' reports about the results in selected research papers recommended by the lecturer. The list of topics includes the following: stochastic processes, stochastic games, automatic verification of software, formal models and specification languages, model-checking, infinite-state systems, etc.
**Syllabus**- probability theory: stochastic processes, Markov chains, continuous-time Markov chains, discrete stochastic programming.
- temporal logic: linear-time and branching-time logics, probabilistic extensions, model-checking
- static analysis: basic concepts, control-flow and data-flow analysis, applications and tools
- game theory: basic game theory, min-max theorem, Nash theorem, games in formal verification, Martin's theorem, stochastic games.

**Literature**- KLEINBERG, Jon and Éva TARDOS.
*Algorithm design*. Boston: Pearson/Addison-Wesley, 2006. xxiii, 838. ISBN 0321295358. info - PUTERMAN, Martin L.
*Markov decision processes : discrete stochastic dynamic programming*. Hoboken, N.J.: Wiley-Interscience, 2005. xvii, 649. ISBN 0471727822. info - DAHLQUIST, Germund, Ned ANDERSON and Åke BJÖRCK.
*Numerical methods*. Mineola, N.Y.: Dover Publications, 2003. xviii, 573. ISBN 0486428079. info - GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE.
*Model checking*. Cambridge: MIT Press, 1999. xiv, 314. ISBN 0262032708. info - FILAR, Jerzy A. and Koos VRIEZE.
*Competitive Markov decision processes : with 57 illustrations*. New York: Springer, 1997. xii, 393. ISBN 0387948058. info - NORRIS, J. R.
*Markov chains*. 1st pub. Cambridge: Cambridge University Press, 1997. xvi, 237. ISBN 9780521481816. info - OWEN, Guillermo.
*Game theory*. 3rd ed. San Diego: Academic Press, 1995. xii, 447. ISBN 0125311516. info - FELLER, William.
*An introduction to probability theory and its applications.*3rd ed. [New York]: John Wiley & Sons, 1968. xviii, 509. ISBN 9780471257080. info

- KLEINBERG, Jon and Éva TARDOS.
**Teaching methods**- Lectures, class discussion, reading.
**Assessment methods**- Oral exam.
**Language of instruction**- Czech
**Listed among pre-requisites of other courses****DEMBSY**Embedded systems

!NOWANY(DFOME,DMKZI,DPGZO,DMPOS,DMZDD,DPITS,DZPJUI,DPOSO,DRPSEC)**DMKZI**Quantum Information Processing Methods

!NOWANY(DEMBSY,DFOME,DPGZO,DMPOS,DMZDD,DPITS,DZPJUI,DPOSO,DRPSEC)**DMPOS**Computer Networks Methods

!NOWANY(DEMBSY,DFOME,DMKZI,DPGZO,DMZDD,DPITS,DZPJUI,DPOSO,DRPSEC)**DMZDD**Digital Data Processing Methods

!NOWANY(DEMBSY,DFOME,DMKZI,DPGZO,DMPOS,DPITS,DZPJUI,DPOSO,DRPSEC)**DPGZO**Computer Graphics and Image Processing

!NOWANY(DEMBSY,DFOME,DMKZI,DMPOS,DMZDD,DPITS,DZPJUI,DPOSO,DRPSEC)**DPITS**Enterprise IT Systems and Services

!NOWANY(DEMBSY,DFOME,DMKZI,DPGZO,DMPOS,DMZDD,DZPJUI,DPOSO,DRPSEC)**DPOSO**Advances in Concurrency

!NOWANY(DEMBSY,DFOME,DMKZI,DPGZO,DMPOS,DMZDD,DPITS,DZPJUI,DRPSEC)**DRPSEC**Research project in computer security

!NOWANY(DEMBSY,DFOME,DMKZI,DPGZO,DMPOS,DMZDD,DPITS,DZPJUI,DPOSO)**DZPJUI**Advanced Methods for Natural Language Processing and Artificial Intelligence

!NOWANY(DEMBSY,DFOME,DMKZI,DPGZO,DMPOS,DMZDD,DPITS,DPOSO,DRPSEC)

- Enrolment Statistics (Spring 2011, recent)
- Permalink: https://is.muni.cz/course/fi/spring2011/DFOME