Benjamin Lucien Kaminski

Benjamin Lucien Kaminski is a Professor at Saarland University and a Lecturer at University College London. He specializes in quantitative aspects of formal program verification, with a focus on probabilistic and quantum programs, incorrectness logic, and non-classical computation models.

His research includes semantics, probabilistic program verification, expected runtimes, and explainable verification. He leads the Examination Board for B.Sc. Computer Science (English) and actively mentors PhD, Master’s, and Bachelor’s students in logic and verification.

• 2025: A Taxonomy of Hoare-Like Logics (POPL), Partial Incorrectness Logic (TPSA)
• 2024: Quantitative Weakest Hyper Pre (OOPSLA), Caesar: A Verifier for Probabilistic Programs (Dafny), Hoare-Like Triples (Incorrectness-track)
• 2023: A Deductive Verification Infrastructure (OOPSLA), Lower Bounds (OOPSLA), A Calculus for Amortized Expected Runtimes (POPL)

He has received notable awards including the Ackermann Award (2020), Best Paper at LOPSTR 2020, and EATCS Best Paper Award at ETAPS 2016. He has also served on program committees for leading conferences like CAV, POPL, and LICS, and reviewed for prestigious journals such as Journal of the ACM and TOCL.