See also my Google Scholar profile.
-
AI Coding Benchmarks Need Proofs, Not Just Tests[PDF]. Daneshvar Amrollahi, Mahyar Karimi, Brando Miranda, Leni Aniva, Chuyue Sun, Clark Barrett, Sanmi Koyejo. Preprint, 2026. -
Faithful Autoformalization via Roundtrip Verification and Repair[PDF]. Daneshvar Amrollahi, Jerry Lopez, Clark Barrett. Preprint, 2026. -
VeriBench: End-to-End Formal Verification Benchmark for AI Coding Agents in Lean 4[PDF]. Brando Miranda, Srivatsava Daruru, Ethan S. Hersch, Zhanke Zhou, Allen Nie, Daneshvar Amrollahi, Leni Aniva, Iddah Mlauzi, Kirill Acharya, Elyas Obbad, Dilara Soylu, Weston Kirk, Zixiao Jolene Wang, Kai Fronsdal, Ying Li, Donald Poindexter Jr., Rakshit Kaushik, Shurui Liu, Yegor Denisov-Blanch, Steven Dillmann, Simon Obstbaum, Santiago Cuellar, John Sarracino, Rylan Schaeffer, Mo Tiwari, Donghyun Lee, Bo Han, Sanmi Koyejo. Preprint, 2026. -
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus[PDF]. Chuyue Sun, Yican Sun, Daneshvar Amrollahi, Ethan Zhang, Shuvendu Lahiri, Shan Lu, David Dill, Clark Barrett. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2026. -
Towards SMT Solver Stability via Input Normalization[PDF]. Daneshvar Amrollahi, Mathias Preiner, Aina Niemetz, Andrew Reynolds, Moses Charikar, Cesare Tinelli, Clark Barrett. Formal Methods in Computer-Aided Design (FMCAD), 2025. -
(Un)Solvable Loop Analysis[PDF]. Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovič. Formal Methods in System Design, 2024. -
Synthesis of Recursive Programs in Saturation[PDF]. Petra Hozzová, Daneshvar Amrollahi, Márton Hajdu, Laura Kovács, Andrei Voronkov, Eva Maria Wagner. International Joint Conference on Automated Reasoning (IJCAR), 2024. -
Algebra-Based Reasoning for Loop Synthesis[PDF]. Andreas Humenberger, Daneshvar Amrollahi, Nikolaj Bjørner, Laura Kovács. Formal Aspects of Computing, 2022. -
Solving Invariant Generation for Unsolvable Loops. Daneshvar Amrollahi, Ezio Bartocci, George Kenison, Laura Kovács, Marcel Moosbrugger, Miroslav Stankovič. International Static Analysis Symposium (SAS), 2022. Radhia Cousot Best Paper Award.