Dr. Yoni Zohar

At any given moment, millions of users worldwide are performing actions across various software systems. Behind every such action  lies complex code that must be flawless: a minor error could lead to widespread disruptions. To prevent errors at such a scale, human testing alone is insufficient; mathematical tools are required to automatically prove the correctness of the code. Dr. Yoni Zohar develops such tools, which are used by leading tech companies to ensure the reliability of their software systems.

His research focuses on Formal Verification and specifically on Satisfiability Modulo Theories (SMT) Solvers—algorithms capable of solving complex logical and mathematical problems in a short time. His work moves between mathematical logic and practical applications, influencing the way software systems are tested and guaranteed to function correctly, even under complex conditions.

Key Research Areas:

• SMT Solvers: Satisfiability Modulo Theories.

• Automated Reasoning: Mathematical logic and automated inference.

• Formal Verification: Ensuring the correctness of software systems.

• Smart Contract Verification: Security and reliability in blockchain technologies.

Research Nature:

 Theoretical-Applied: Addressing open questions in mathematical logic while developing tools used by world-leading technology companies.

Career Path:

 Graduates of the lab can transition into diverse high-level roles:

• Industry: Developers of verification  tools in top-tier tech companies.

• Academia: Researchers and lecturers in the fields of logic and formal verification.

• Entrepreneurship: Developers of tools for AI code verification and smart contracts.