TLA+ model checking made symbolic. - Igor Konnov 001; Jure Kukovec; Thanh-Hai Tran 002 (Proc. ACM Program. Lang., 2019)

Cutoffs for Symmetric Point-to-Point Distributed Algorithms. - Thanh-Hai Tran 002; Igor Konnov 001; Josef Widder (NETYS, 2020)

Extracting symbolic transitions from TLA+ specifications. - Jure Kukovec; Thanh-Hai Tran 002; Igor Konnov 001 (Sci. Comput. Program., 2020)

A case study on parametric verification of failure detectors. - Thanh-Hai Tran 002; Igor Konnov 001; Josef Widder (Log. Methods Comput. Sci., 2023)

Technical Report: Exploring Automatic Model-Checking of the Ethereum specification. - Igor Konnov 001; Jure Kukovec; Thomas Pani; Roberto Saltini; Thanh-Hai Tran 002 (CoRR, 2025)