Formula Normalizations in Verification. - Simon Guilloud; Mario Bucev; Dragana Milovancevic; Viktor Kuncak (CAV (3), 2023)

Proving and Disproving Equivalence of Functional Programming Assignments. - Dragana Milovancevic; Viktor Kuncak (Proc. ACM Program. Lang., 2023)

Proving Termination via Measure Transfer in Equivalence Checking. - Dragana Milovancevic; Carsten Fuhs; Mario Bucev; Viktor Kuncak (IFM, 2024)

Formal Autograding in a Classroom. - Dragana Milovancevic; Mario Bucev; Marcin Wojnarowski; Samuel Chassot; Viktor Kuncak (ESOP (2), 2025)