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