I am an Assistant Professor in the Computer Science Department at the Technion – Israel Institute of Technology. My research is in the formal verification of hardware and software systems, and the interactions between them.
We are entering an era in which AI — and large language models in particular — will increasingly generate hardware designs and programs directly from a specification, in essentially any HDL or programming language a developer chooses. This makes my work more relevant than ever: machine-generated artifacts cannot simply be trusted, and formal verification is what turns them into systems we can rely on.
Computer Science Department · Taub Building, Room 627 · Technion, Haifa, Israel
My research program in formal verification has been awarded a 2025 European Research Council (ERC) Consolidator Grant.
Read more: Technion News · Ynet (Hebrew)
Funded by the European Union (European Research Council, ERC). Views and opinions expressed are those of the author only and do not necessarily reflect those of the European Union or the ERC.
Formally verifying that a system conforms to its specification is one of the most challenging problems in computer science — so challenging that some instances are undecidable. Yet over the past two decades the field has advanced substantially, turning once-theoretical ideas into tools that verify real hardware and software.
This matters more than ever as code is increasingly produced by AI. There is a growing expectation that, in the near future, large language models will generate hardware designs and programs from a high-level specification, in any HDL or programming language a developer chooses. But LLMs hallucinate — and a hallucinating model can produce subtly buggy hardware or software just as readily as correct code. Their outputs cannot be taken on trust.
This is exactly where formal methods become indispensable. Rather than trusting machine-generated code, we can check it against its specification with a formal verification engine — model checking, theorem proving, and related techniques — and obtain a mathematical guarantee that it behaves as intended. As industry shifts toward automatically generated code at scale, the ability to formally verify that code carries enormous practical and economic value.
My goal is to create innovative tools and techniques that make this kind of verification practical, helping engineers build better, safer, and more trustworthy digital systems — even when much of the code is written by machines.
I am looking for graduate students who would like to take on the next formal verification challenge. If this area interests you, please get in touch.
Our paper “Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?” was accepted to IJCAI 2026. It studies how large language models can assist in constructing induction proofs for hardware verification. Please contact us to learn more.
Our group works across the theory and practice of verification. Current directions include:
The best way to reach me is by email. I am happy to hear from prospective students, collaborators, and colleagues.
Email meInquiries about graduate positions are always welcome — please include a short note about your background and interests.
