Formalizing Fibonacci Squares (short paper). - Muhammad Harun Ali Khan 001 (CICM Workshops, 2021)

Robust Mean Estimation by All Means (Short Paper). - Reynald Affeldt; Clark W. Barrett; Alessandro Bruni; Ieva Daukantas; Harun Khan 001; Takafumi Saikawa; Carsten Schürmann (ITP, 2024)

lean-smt: An SMT Tactic for Discharging Proof Goals in Lean. - Abdalrhman Mohamed; Tomaz Mascarenhas; Harun Khan 001; Haniel Barbosa; Andrew Reynolds 001; Yicheng Qian; Cesare Tinelli; Clark W. Barrett (CAV (3), 2025)

Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. - Abdalrhman Mohamed; Tomaz Mascarenhas; Muhammad Harun Ali Khan 001; Haniel Barbosa; Andrew Reynolds 001; Yicheng Qian; Cesare Tinelli; Clark W. Barrett (Zenodo, 2025)

Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. - Abdalrhman Mohamed; Tomaz Mascarenhas; Muhammad Harun Ali Khan 001; Haniel Barbosa; Andrew Reynolds 001; Yicheng Qian; Cesare Tinelli; Clark W. Barrett (Zenodo, 2025)

Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. - Abdalrhman Mohamed; Tomaz Mascarenhas; Muhammad Harun Ali Khan 001; Haniel Barbosa; Andrew Reynolds 001; Yicheng Qian; Cesare Tinelli; Clark W. Barrett (Zenodo, 2025)

bv_decide SMT-COMP 2025 Submission. - Henrik Böving; Siddharth Bhat; Alex C. Keizer; Luisa Cicolini; Léon Frénot; Abdalrhman Mohamed; Léo Stefanesco; Harun Khan 001; Joshua Clune; Clark W. Barrett; Tobias Grosser (Zenodo, 2025)

bv_decide SMT-COMP 2025 Submission. - Henrik Böving; Siddharth Bhat; Alex C. Keizer; Luisa Cicolini; Léon Frénot; Abdalrhman Mohamed; Léo Stefanesco; Harun Khan 001; Joshua Clune; Clark W. Barrett; Tobias Grosser (Zenodo, 2025)

bv_decide SMT-COMP 2025 Submission. - Henrik Böving; Siddharth Bhat; Alex C. Keizer; Luisa Cicolini; Léon Frénot; Abdalrhman Mohamed; Léo Stefanesco; Harun Khan 001; Joshua Clune; Clark W. Barrett; Tobias Grosser (Zenodo, 2025)

bv_decide SMT-COMP 2025 Submission. - Henrik Böving; Siddharth Bhat; Alex C. Keizer; Luisa Cicolini; Léon Frénot; Abdalrhman Mohamed; Léo Stefanesco; Harun Khan 001; Joshua Clune; Clark W. Barrett; Tobias Grosser (Zenodo, 2025)

Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean. - Abdalrhman Mohamed; Tomaz Mascarenhas; Muhammad Harun Ali Khan 001; Haniel Barbosa; Andrew Reynolds 001; Yicheng Qian; Cesare Tinelli; Clark W. Barrett (Zenodo, 2025)