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:

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

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.