software engineering

Formal Methods

Formal methods is an interdisciplinary area, where the research can combine research in security, algorithms, genetic algorithms and other areas.

03-7384056 / 03-5318629
Room 280 / Building 216
Open door
14:00 - 16:00 | Monday and Tuesday

Over 50% of the effort in developing software and hardware nowadays is devoted to testing and verifying its reliability. This involves using software engineering methods, and developing and applying algorithms for automatically checking software and hardware against its specification. Some research topics of this group are:

  • Model checking: the automatic verification of software and hardware.
  • Testing: manually or automatically checking the code against its specification.
  • Theorem proving: using logic to verify the correctness of systems.
  • Specification: how to formally specify systems.
  • Synthesis: developing a system directly (automatically) from specification.

The research includes theoretical studies of automatic verification, theorem proving, logic, automata theory, as well as the development of tools. Formal methods is an interdisciplinary area, where the research can combine research in security, algorithms, genetic algorithms and other areas.