I am a senior scientist (≈assistant professor) in the Faculty of Mathematics and Computer Science at the Weizmann Institute of Science. I joined Weizmann in September 2024, and before that I was a researcher at VMware Research Group, a postdoc in Alex Aiken's group at Stanford University, and a PhD student at Tel Aviv University advised by Mooly Sagiv.
I am recruiting MSc students, PhD students, and postdocs — feel free to reach out! If you are a student at Weizmann, I am teaching an introduction to verification course in Spring 2025.
I have broad research interests in programming languages, verification, formal methods, logic, and distributed systems.
The main theme of my research is developing algorithms and methodologies that can make verification of realistic software systems practical. My emphasis is on automated techniques that reduce the tedious parts of systems verification and are designed for fruitful cooperation with the user, acknowledging the fact that automation failure is the dominant case in the development process of verified systems. I like to design techniques that are principled rather than heuristic whenever possible, employing concepts such as decomposition, decidable logics, and primal-dual algorithms. The main application domain I have considered is distributed systems, and I have recently worked on verifying other critical systems such as storage systems and cluster management systems.
Another theme of my research is developing optimization and verification techniques for emerging domains such as deep neural networks and quantum computing. A recent theme is using large languages models for verification.
I am grateful to be supported by an Azrieli Early Career Faculty Fellowship.
Top Links
You may be interested in:
Ivy a system for verifying safety and liveness of distributed algorithms and distributed system implementations using decidable logics.
mypyvy a research platform for verification of infinite-state systems focusing on automated invariant inference, inspired by Ivy.
Verus a program verifier for Rust that aims to verify rich functional correctness specifications for realistic systems code at scale.
TASO Tensor Algebra SuperOptimizer that optimizes deep learning computations using automatically generated and verified graph transformations, achieving up to 3x speedup over other frameworks.
Quartz a superoptimizer for quantum circuits that automatically generates, verifies, and applies circuit transformations, outperforming other quantum circuit optimizers on a range of quantum gate sets.
How far can you EPR? a 30 minute talk summarizing my PhD research given at the virtual ETAPS 2020 Afternoon upon receiving the 2020 ETAPS Doctoral Dissertation Award.