Harun Khan

According to our database, Harun Khan authored at least 13 papers between 2021 and 2026.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2026

Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions.

Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli

Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2026

2025

Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean.

Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett

Dataset, June, 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, Joshua Clune, Clark W. Barrett, Tobias Grosser

Dataset, June, 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, Joshua Clune, Clark W. Barrett, Tobias Grosser

Dataset, June, 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, Joshua Clune, Clark W. Barrett, Tobias Grosser

Dataset, June, 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, Joshua Clune, Clark W. Barrett, Tobias Grosser

Dataset, June, 2025

Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean.

Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett

Dataset, May, 2025

Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean.

Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett

Dataset, April, 2025

Artifact #305 CAV25 - Lean-SMT: An SMT tactic for discharging proof goals in Lean.

Abdalrhman Mohamed, Tomaz Mascarenhas, Muhammad Harun Ali Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett

Dataset, April, 2025

Interactive Bitvector Reasoning using Verified Bit-Blasting.

Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex C. Keizer, Léon Frénot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark W. Barrett, Tobias Grosser

Proc. ACM Program. Lang., 2025

lean-smt: An SMT Tactic for Discharging Proof Goals in Lean.

Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark W. Barrett

Proceedings of the Computer Aided Verification - 37th International Conference, 2025

2024

Robust Mean Estimation by All Means (Short Paper).

Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2021

Formalizing Fibonacci Squares (short paper).

Muhammad Harun Ali Khan

Proceedings of the Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26, 2021