I am a 3rd-year Computer Science PhD student at Stanford University, advised by Clark Barrett.
My interests center on combining automated reasoning with large language models (LLMs). More specifically, I work on autoformalization, the use of LLMs to translate natural language into machine-checkable formal statements.
Previously, I worked on a range of formal methods topics: SMT solvers, theorem provers, loop invariants, program synthesis, and verifying software network functions.
Feel free to reach out if you would like to chat or collaborate.
Email: daneshvar [at] cs [dot] stanford [dot] edu
I am looking for Summer 2027 internships!
News
[08.2026]: Faithful Autoformalization via Roundtrip Verification and Repair accepted at Findings of ACL: EMNLP 2026.
[06.2026]: Joining Uber Technologies, Inc. as a PhD Software Engineer Intern in Seattle, Washington.
[06.2026]: AI Coding Benchmarks Need Proofs, Not Just Tests accepted at DL4C and AI4Math, ICML 2026.
[06.2026]: Faithful Autoformalization via Roundtrip Verification and Repair accepted at AI4Math, ICML 2026.
[06.2026]: VeriBench: End-to-End Formal Verification Benchmark for AI Coding Agents in Lean 4 accepted at DL4C and AI4Math, ICML 2026.
[06.2026]: Know Your Limits: On the Faithfulness and Failure Modes of LLM Autoformalization accepted at AI4Math and AI4Law, ICML 2026.
[07.2025]: Towards SMT Solver Stability via Input Normalization accepted at FMCAD 2025.
[06.2025]: Joined the Automated Reasoning Group at Amazon Web Services (AWS) in Santa Clara, California as an Applied Science Intern.
[06.2025]: Passed my PhD qualifying exam and earned a Master’s in Computer Science.
[08.2024]: Gave a talk Towards Improved Stability for SMT Solvers at the CENTAUR annual meeting, Stanford University.
[03.2024]: Synthesis of Recursive Programs in Saturation accepted at IJCAR 2024.
[01.2024]: Started my PhD in Computer Science at Stanford University.