translated by Google

Formal Methods for Analysis and Verification

Subcategories:

Formal verification and analysis of sequential programs

Annotation:
The most common technique for detecting bugs in programs is still testing that makes it easy to find many bugs, but does not make it possible to prove the flawlessness of the program. This is the method of formal verification. Analytical methods can then be used to get information that will allow for example optimization during compilation or more effective troubleshooting in programs. The question covers the basic techniques of program analysis and verification.

Warp:
Formal aspects of testing, extent of code coverage 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.

Tutor: doc. Jan Strejček, prof. Jiří Barnat

Other Recommended Literature:


Verification and analysis of parallel programs and reactive systems

Annotation:
The development of reactive, parallel, or otherwise distributed systems is more difficult and costly than sequential programs. The primary reason for this claim is the fact that the errors of design or implementation of these systems are manifested at random. As part of this question, the student will become familiar with the complete technology of analyzing and verifying the systems by using the model verification method.

Warp:
Modeling and concurrent and reactive systems, formal requirements specification by LTL and CTL logic, the use of automata theory to implement the method, conversion of formal specification to omega-regular automata, enumeration and symbolic approaches to model validation method, problem of state space generation, representation of the state space, tools for implementing the 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)

Tutor: prof. Ivana Černá, prof. Jiří Barnat, doc. Jan Strejček

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 endless-state systems

Annotation:
Some real-world SW systems need to be modeled as infinitely state-like. The candidate will learn about the possibilities and basic methods of (end) specification of systems with infinitely many states and the (algorithmic) limits of automatic verification of the properties of these systems.

Warp:
Methods of Process Specification, Equivalence of Processes, Decision-Making of Equivalence Problems, Verification of Model of Endless-state Systems.

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 pp.
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.

Tutor: prof. Mojmír Křetínský

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 In JABergstra et al .: Handbook of Process Algebra, Elsevier, 2001, p.3-100

Modeling and verifying hybrid systems and real-time systems

Annotation:
The interaction of software systems with the real physical world often enforces requirements beyond the logical accuracy of developed systems. Typical examples are requirements for, for example, hard time constraints. Students will be introduced to modeling formalisms for describing such systems and methods of their analysis.

Warp:
Hybrid automata, decisionability of accessibility problem, time automata, regional and zone abstraction, verification of temporal properties of time machines.

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

Tutor: prof. Jiří Barnat

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


Annotation:
Student will be acquainted with basic methods and techniques from the use of modal and temporal logic formal vallidation and verification of computer systems.

Warp:
Logic of linear time - variants of logic, axiomatization, decisiveness and complexity, examples of use, logic of branch time - axiomatization, decisionability and complexity, examples of use, modal calculus - syntax and semantics, alternative of fixed points, expression of properties.

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

Tutor: prof. Luboš Brim, doc. Jan Strejček, prof. Jiří Barnat

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.