• The 2007
CADE Skolem Award for the paper "Efficient E-Matching for SMT Solvers" that has passed the test of time, by being a most influential paper in the field. • The 2021
Computer Aided Verification Award for the field-changing contributions regarding his work on
Z3. • The 2025
CADE Skolem Award for the paper "The Lean Theorem Prover (System Description)" that has passed the test of time, by being a most influential paper in the field. ==References==