Daneshvar Amrollahi

I am a 3^rd-year Computer Science PhD student at Stanford University, advised by Clark Barrett.

My interests center on combining formal reasoning with large language models (LLMs), especially through autoformalization (translating natural language into formal representations for rigorous reasoning and verification). More specifically, I have been working on the faithfulness of LLMs in autoformalization, and verifying code generated by LLMs using Lean.

Previously, I have worked on SMT solvers, theorem provers, loop invariant generation, program synthesis, and verifying software network functions.

Email: daneshvar [at] cs [dot] stanford [dot] edu

News

• [July 2025]: Our paper “Towards Improved Stability for SMT Solvers via Input Normalization” got accepted to FMCAD 2025.
• [June 2025]: Joined the Automated Reasoning Group of Amazon Web Services (AWS) in Santa Clara, California as an Applied Science Intern.
• [June 2025]: Passed my PhD qualifications exam and earned a Master’s degree in Computer Science.
• [Aug 2024]: Gave a talk Towards Improved Stability for SMT Solvers at the Center for Automated Reasoning (CENTAUR) annual meeting, Stanford University.
• [March 2024]: Our paper “Synthesis of Recursive Programs in Saturation” got accepted to IJCAR 2024.
• [Jan 2024]: Started my PhD in Computer Science at Stanford University.

Blog

• 2026/02/22 We Traded Beauty for Convenience
• 2025/07/23 Why Are We Still So Skeptical About LLMs?
• 2025/04/06 The Antidote Is Difficulty
• 2024/11/26 Using a Linux Laptop as a Hotspot for a PS5
• 2023/11/04 First Post