Mechanizing Matching Logic in Coq. - Péter Bereczky; Xiaohong Chen 002; Dániel Horpácsi; Tamás Bálint Mizsei; Lucas Peña; Jan Tusil (FROM, 2022)

Interactive Matching Logic Proofs in Coq. - Jan Tusil; Péter Bereczky; Dániel Horpácsi (ICTAC, 2023)

Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties. - Jan Tusil; Traian Serbanuta; Jan Obdrzálek (LPAR, 2023)

Minuska: Towards a Formally Verified Programming Language Framework. - Jan Tusil; Jan Obdrzálek (SEFM, 2024)