Quantitative Verification Group

The paper Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers by Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, and Alexandra Silva has been accepted at OOPSLA 2024. The paper presents a novel weakest pre calculus for reasoning about quantitative hyperproperties over nondeterministic and probabilistic programs.

The paper “A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests” by Lena Verscht and Benjamin Kaminski has been accepted for the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2025) in Denver. The paper provides an overview of program logics, including Hoare…

The paper entitled “Lower Bounds for Possibly Divergent Probabilistic Programs” by Shenghua Feng (ISCAS, China), Mingshuai Chen (Zhejiang University, China), Han Su (ISCAS, China), Benjamin Kaminski, Joost-Pieter Katoen (RWTH Aachen), and Naijun Zhan (ISCAS, China) has been accepted for presentation at the OOPSLA issue of the Proceedings of the ACM on Programming Languages 2023. The paper presents…

The paper entitled “A Calculus for Amortized Expected Runtimes” by Kevin Batz (RWTH Aachen), Benjamin Kaminski, Joost-Pieter Katoen (RWTH Aachen), Christoph Matheja (DTU Lyngby) and Lena Verscht has been accepted for presentation at the 50th ACM Symposium on Principles of Programming Languages (POPL). The paper presents a weakest precondition-style calculus to determine the amortized expected…