Field of study: Formal methods for analysis and verification

Sub-circles:

• Formal verification and analysis of sequential programs
• Verification and analysis of parallel programs and reactive systems
• Specification and verification of infinite-state systems
• Modeling and verification of hybrid and real-time systems
• Modal and temporal logics

Formal verification and analysis of sequential programs

Annotation:
The most common technique for detecting errors in programs is still testing, which allows you to easily find many errors, but does not allow you to prove that the program is error-free. Formal verification methods are used for this. Analysis methods can then be used to obtain information that allows, for example, optimization during compilation or more effective search for errors in programs. The question covers the basic techniques of program analysis and verification.

Warp:
Formal aspects of testing, code coverage measures, deductive and axiomatic program verification, static analysis and abstract interpretation, symbolic execution.

Basic study material:
Doron A. Peled: Software Reliability Methods (Chapters 7 and 9)
Flemming Nielson, Hanne R. Nielson, and Chris Hankin: Principles of Program Analysis (Chapters 2 and 4)
James C. King, Symbolic execution and program testing, Communications of the ACM, volume 19, number 7, 1976, 385--394.

Examiner: prof. RNDr. Jan Strejček, Ph.D. , prof. RNDr. Jiří Barnat, Ph.D.

Verification and analysis of parallel programs and reactive systems

Annotation:
The development of reactive, parallel, or otherwise distributed systems is an order of magnitude more difficult and expensive than sequential programs. The primary reason for this statement is the fact that design or implementation errors in these systems manifest themselves randomly. In this question, the student will become familiar with the complete technology of analysis and verification of the aforementioned systems using the model checking method.

Warp:
Modeling of concurrent and reactive systems, formal specification of requirements using LTL and CTL logics, use of automata theory for method implementation, conversion of formal specification to omega-regular automata, enumerative and symbolic approaches to the model verification method, state space generation problem, state space reduction methods, state space representation, tools for implementing verification methods and their implementation.

Basic study material:
Doron A. Peled: Software Reliability Methods (Chapters 4-6)
Clarke, Grumberg, Peled: Model checking (Chapters 2-6,8-10)

Examiner: prof. RNDr. Ivana Černá, CSc. , prof. RNDr. Jiří Barnat, Ph.D. , prof. RNDr. Jan Strejček, Ph.D.

Other recommended literature:
C. Baier, JP Katoen: Principles of Model Checking
Gerard J. Holzmann: The Spin model checker, primer and reference manual

Specification and verification of infinite-state systems

Annotation:
Some real SW systems must be modeled as infinite states. The candidate will become familiar with the issues of what are the possibilities and basic methods of (finite) specification of systems with infinitely many states and what are the (algorithmic) limits of automatic verification of the properties of these systems.

Warp:
Methods of process specification, Process equivalence, Decidability of equivalence problems, Model verification of infinite-state systems.

Basic study material:
Javier Esparza: Grammars as Processes. Formal and Natural Computing 2002, p. 277-297
Wan Fokkink: Introduction to Process Algebra, Springer, 2000, 163 p.
O. Burkart, D. Caucal, F. Moller, B. Steffen: Verification on infinite structures. In JA Bergstra et al.: Handbook of Process Algebra, Elsevier, 2001, p. 545-626.

Examiner: prof. RNDr. Jan Strejček, Ph.D.

Other recommended reading:
J.Srba: Infinite Results Roadmap
Doron A. Peled: Software Reliability Methods (Chapter 8)
RJvan Glabbeck: The linear time - branching time spectrum I. In JABergstra et al.: Handbook of Process Algebra, Elsevier, 2001, p.3-100

Modeling and verification of hybrid and real-time systems

Annotation:
The interaction of software systems with the real physical world often imposes requirements that go beyond the logical correctness of the developed systems. A typical example is requirements related to, for example, hard time constraints. In this question, students will become familiar with modeling formalisms for describing such systems and methods for their analysis.

Warp:
Hybrid automata, decidability of the reachability problem, temporal automata, regional and zone abstraction, verification of temporal properties of temporal automata.

Basic study material:
T. Henzinger: The Theory of Hybrid Automata
C. Baier, JP Katoen: Principles of Model Checking (Chapter 9)

Examiner: prof. RNDr. Jiří Barnat, Ph.D. , doc. RNDr. David Šafránek, Ph.D.

Other recommended literature:
John Lygeros: Lecture Notes on Hybrid Systems
Waez, Dingel, Rudie: Timed Automata for the Development of Real-Time Systems

Modal and temporal logics

Annotation:
The student will become familiar with basic methods and techniques in the field of using modal and temporal logics for formal validation and verification of computer systems.

Warp:
Propositional modal logic, dynamic logic, Linear time logics - variants of logics, axiomatization, decidability and complexity, examples of use, Branching time logics - axiomatization, decidability and complexity, examples of use, Modal mu-calculus - syntax and semantics, fixed point alternation, expression of properties.

Basic study material:
C. Stirling, Modal and temporal properties of processes. Springer, 2001.

Examiner: prof. RNDr. Jan Strejček, Ph.D. , prof. RNDr. Jiří Barnat, Ph.D.

Other recommended literature:
C. Baier, J.-P. Cotton. Principles of model checking. MIT Press, 2008.
O. Grumberg, D. Peled, E. Clarke. Model checking. Cambridge: MIT Press, 1999.