Solving Invariant Generation for Unsolvable Loops. - Daneshvar Amrollahi; Ezio Bartocci; George Kenison; Laura Kovács; Marcel Moosbrugger; Miroslav Stankovic (SAS, 2022)

Algebra-Based Reasoning for Loop Synthesis. - Andreas Humenberger; Daneshvar Amrollahi; Nikolaj S. Bjørner; Laura Kovács (Formal Aspects Comput., 2022)

An Encoding for CLP Problems in SMT-LIB. - Daneshvar Amrollahi; Hossein Hojjat; Philipp Rümmer (LSFA/HCVS, 2023)

Synthesis of Recursive Programs in Saturation. - Petra Hozzová; Daneshvar Amrollahi; Márton Hajdú; Laura Kovács; Andrei Voronkov; Eva Maria Wagner (IJCAR (1), 2024)

Using Normalization to Improve SMT Solver Stability. - Daneshvar Amrollahi; Mathias Preiner; Aina Niemetz; Andrew Reynolds 001; Moses Charikar; Cesare Tinelli; Clark W. Barrett (CoRR, 2024)

(Un)Solvable loop analysis. - Daneshvar Amrollahi; Ezio Bartocci; George Kenison; Laura Kovács; Marcel Moosbrugger; Miroslav Stankovic (Formal Methods Syst. Des., 2025)

VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. - Chuyue Sun; Yican Sun; Daneshvar Amrollahi; Ethan Zhang; Shuvendu K. Lahiri; Shan Lu 001; David L. Dill; Clark W. Barrett (CoRR, 2025)