Büchi Complementation. - Julian Brunner 001 (Arch. Formal Proofs, 2017)

Transition Systems and Automata. - Julian Brunner 001 (Arch. Formal Proofs, 2017)

Partial Order Reduction. - Julian Brunner 001 (Arch. Formal Proofs, 2018)

Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. - Julian Brunner 001; Peter Lammich (J. Autom. Reason., 2018)

A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. - Julian Brunner 001; Benedikt Seidl; Salomon Sickert (ITP, 2019)

Formal Verification of Executable Complementation and Equivalence Checking for Büchi Automata. - Julian Brunner 001 (IFM, 2020)

Formal Verification of Algorithms for Automata and Model Checking. - Julian Brunner 001 (2022)