Destabilizing Iris
S. Spies, N. Mück, H. Zeng, M.J. Sammler, A. Lattuada, P. Müller, D. Dreyer, Proceedings of the ACM on Programming Languages 9 (2025) 848–873.

Quantitative bounds on resource usage of probabilistic programs
K. Chatterjee, A.K. Goharshady, T. Meggendorfer, D. Zikelic, Proceedings of the ACM on Programming Languages 8 (2024).

Equivalence and similarity refutation for probabilistic programs
K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, Proceedings of the ACM on Programming Languages 8 (2024).

CQS: A formally-verified framework for fair and abortable synchronization
N. Koval, D. Khalanskiy, D.-A. Alistarh, Proceedings of the ACM on Programming Languages 7 (2023).

Transitioning from structural to nominal code with efficient gradual typing
F. Mühlböck, R. Tate, Proceedings of the ACM on Programming Languages 5 (2021).

The reads-from equivalence for the TSO and PSO memory models
T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings of the ACM on Programming Languages 5 (2021).

Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time
P. Wang, H. Fu, K. Chatterjee, Y. Deng, M. Xu, in:, Proceedings of the ACM on Programming Languages, ACM, 2020.

Value-centric dynamic partial order reduction
K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, ACM, 2019.

Data-centric dynamic partial order reduction
M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings of the ACM on Programming Languages 2 (2018).

A new proof rule for almost-sure termination
A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).

Optimal Dyck reachability for data-dependence and Alias analysis
K. Chatterjee, B. Choudhary, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 2 (2017).