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.
See the group website for more information: http://u.cs.biu.ac.il/~doronp/formalmethods.html