Computing Inductive Invariants of Regular Abstraction Frameworks. - Philipp Czerner; Javier Esparza; Valentin Krasotin; Christoph Welzel-Mohr (CONCUR, 2024)

A Resolution-Based Interactive Proof System for UNSAT. - Philipp Czerner; Javier Esparza; Valentin Krasotin (FoSSaCS (2), 2024)

dodo. - Christoph Welzel-Mohr; Valentin Krasotin; Philipp Czerner; Javier Esparza (Zenodo, 2024)

Regular Model Checking for Systems with Effectively Regular Reachability Relation. - Javier Esparza; Valentin Krasotin (MFCS, 2025)