Formal Methods -FM@BIU
Join our seminar talks here: Here
FM@BIU studies and develops various techniques to formally verify software and hardware systems. Our research involves both the theoretical study of formal methods and the development of related tools for verification of software and hardware.
Traditional quality assurance methods concentrate on sampling the code and provide weak assurance of correctness. Nowadays, bugs in safety critical systems such as airplanes or trains have enormous consequences. Smart contracts on blockchains transfer actual assets, and therefore rely on the correctness of the underlying code in order to prevent wrong transactions. The methods and tools that we develop are aimed towards comprehensive analysis of systems that would significantly increase the chance of finding errors during the development process.
This includes:
Verification and synthesis of hardware and software
Specification formalisms and temporal logics
Automated reasoning
SAT & SMT tools
Model checking
Automata learning
Testing
Runtime verification
For more information on the subject of Formal Methods in the Department of Computer Science at Bar-Ilan University, contact us and we will get back to you as soon as possible.

Researchers
-
פרופ' פלד דורון
03-5318765 / 03-7384056