Formal methods for analysis and verification

Subheadings:

• 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 makes it easy to find many errors, but does not make it possible 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 will allow, for example, optimization during compilation or more efficient debugging of programs. The question covers the basic techniques of program analysis and verification.

Warp:
Formal aspects of testing, measures of code coverage by tests, 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 that of sequential programs. The primary reason for this statement is the fact that design or implementation errors of these systems are random. Within this question, the student will get acquainted with the complete technology of analysis and verification of these systems by model checking.

Warp:
Modeling and concurrent and reactive systems, formal specification of requirements by LTL and CTL logics, use of automata theory for method implementation, conversion of formal specification to omega-regular automata, enumerative and symbolic approaches to model validation method, state space generation problem, state space reduction methods, state space representation, tools for implementation of verification method 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 get acquainted with the issue of what are the possibilities and basic methods of (final) 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, Verification of infinite state systems model.

Basic study material:
Javier Esparza: Grammars as Processes. Formal and Natural Computing 2002, pp. 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, pp. 545-626.

Examiner: prof. RNDr. Mojmír Křetínský, CSc. , prof. RNDr. Jan Strejček, Ph.D.

Other recommended literature:
J.Srba: Roadmap of Infinite Results
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 the requirements concerning, for example, hard time limits. Within this question, students will get acquainted with modeling formalisms for the description of such systems and methods of their analysis.

Warp:
Hybrid automata, decidability of reachability problem, time automata, regional and zone abstraction, verification of temporal properties of time 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 get acquainted with the basic methods and techniques in the use of modal and temporal logics, formal validation and verification of computer systems.

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

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

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

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