Research
Formal verification, automated reasoning, and program synthesis. The methods that make code provable.
- Verification of Quantitative Hyperproperties Using Trace Enumeration Relations Read on arXiv
- Automatic Rootcausing for Program Equivalence Failures in Binaries Read at Microsoft Research