The Formal Methods Group:
The formal methods group at the Computer Science Department
at Bar Ilan University is led by Prof. Doron A. Peled.
Over 50% of the effort in develping software and hardward 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:
The research includes theorical 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.
- Model checking: the automatic verification of software and hardware.
- Testing: manually or automatically checking the code againts its
- Theorem proving: using logic to verify the correctness of systems.
- Specification: how to formally specify systems.
- Synthesis: develping a system directly (automatically) from