Dr. Hadar Frenkel

Automated Verification, Temporal Logics, and Formal Languages

In safety-critical systems, such as autonomous vehicles, cloud infrastructures, or sensitive data security, a single bug can lead to life-threatening consequences or irreversible damage. Standard testing (QA) only covers scenarios we anticipate, but in complex systems, the number of possible scenarios is enormous and impossible to cover manually. Dr. Frenkel’s research aims to ensure the absence of errors through formal verification, by using mathematical tools to prove that a program adheres to its specification. In addition, Dr. Frenkel develops methods and algorithms to explain the root cause of failures and proposes methods to repair the system accordingly. 

The principles of this research are  currently applied to ensure reliability in complex hardware chips and safety-critical systems.

Primary Research Areas:

• Logics and Automata: Developing formal languages for the specification of complex properties. Developing automata-based verification algorithms, using automata learning. 

• Security and Privacy: Verifying complex Hyperproperties to reason about information flow and security, fairness, and robustness of systems. 

• Explainability and Causal Analysis: Developing tools that allow to find causes and explanations of system behaviours, and, in particular, system failures. 

Research Nature:

The research is primarily theoretical, but includes implementation and coding to evaluate the proposed algorithms.

Career Path:

The field of formal verification has become critical in the semiconductor, cloud, and autonomous systems industries. The lab prepares graduates for dedicated verification positions at industry giants like NVIDIA, Amazon, and IBM, where they ensure the reliability of the world’s most advanced technologies.