PARTY Parameterized Synthesis of Token Rings. - Ayrat Khalimov 001; Swen Jacobs; Roderick Bloem (CAV, 2013)

Towards Efficient Parameterized Synthesis. - Ayrat Khalimov 001; Swen Jacobs; Roderick Bloem (VMCAI, 2013)

Parameterized Model Checking of Token-Passing Systems. - Benjamin Aminof; Swen Jacobs; Ayrat Khalimov 001; Sasha Rubin (VMCAI, 2014)

Parameterized Synthesis Case Study: AMBA AHB. - Roderick Bloem; Swen Jacobs; Ayrat Khalimov 001 (SYNT, 2014)

Specification Format for Reactive Synthesis Problems. - Ayrat Khalimov 001 (SYNT, 2015)

Decidability of Parameterized Verification - Roderick Bloem; Swen Jacobs; Ayrat Khalimov 001; Igor Konnov 001; Sasha Rubin; Helmut Veith; Josef Widder (Morgan & Claypool Publishers, 2015)

Tight Cutoffs for Guarded Protocols with Fairness. - Simon Außerlechner; Swen Jacobs; Ayrat Khalimov 001 (VMCAI, 2016)

The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results. - Swen Jacobs; Roderick Bloem; Romain Brenguier; Ayrat Khalimov 001; Felix Klein 001; Robert Könighofer; Jens Kreber; Alexander Legg; Nina Narodytska; Guillermo A. Pérez 001; Jean-François Raskin; Leonid Ryzhyk; et al. (SYNT@CAV, 2016)

Decidability in Parameterized Verification. - Roderick Bloem; Swen Jacobs; Ayrat Khalimov 001; Igor Konnov 001; Sasha Rubin; Helmut Veith; Josef Widder (SIGACT News, 2016)

Bounded Synthesis for Streett, Rabin, and text CTL^*. - Ayrat Khalimov 001; Roderick Bloem (CAV (2), 2017)

CTL* synthesis via LTL synthesis. - Roderick Bloem; Sven Schewe; Ayrat Khalimov 001 (SYNT@CAV, 2017)

The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants & Results. - Swen Jacobs; Nicolas Basset; Roderick Bloem; Romain Brenguier; Maximilien Colange; Peter Faymonville; Bernd Finkbeiner; Ayrat Khalimov 001; Felix Klein 001; Thibaud Michaud; Guillermo A. Pérez 001; Jean-François Raskin; et al. (SYNT@CAV, 2017)

OpenSEA: Semi-Formal Methods for Soft Error Analysis. - Patrick Klampfl; Robert Könighofer; Roderick Bloem; Ayrat Khalimov 001; Aiman Abu-Yonis; Shiri Moran (CoRR, 2017)

Bounded Synthesis of Register Transducers. - Ayrat Khalimov 001; Benedikt Maderbacher; Roderick Bloem (ATVA, 2018)

Reactive Synthesis: Branching Logics and Parameterized Systems. - Ayrat Khalimov 001 (CoRR, 2018)

Register-Bounded Synthesis. - Ayrat Khalimov 001; Orna Kupferman (CONCUR, 2019)

The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results. - Swen Jacobs; Roderick Bloem; Maximilien Colange; Peter Faymonville; Bernd Finkbeiner; Ayrat Khalimov 001; Felix Klein 001; Michael Luttenberger; Philipp J. Meyer; Thibaud Michaud; Mouhammad Sakr; Salomon Sickert; et al. (CoRR, 2019)

Register Games on Infinite Ordered Data Domains. - Léo Exibard; Emmanuel Filiot; Ayrat Khalimov 001 (CoRR, 2020)

Church Synthesis on Register Automata over Linearly Ordered Data Domains. - Léo Exibard; Emmanuel Filiot; Ayrat Khalimov 001 (STACS, 2021)

Transducer Synthesis from Universal Register Automata in (N, >). - Ayrat Khalimov 001; Emmanuel Filiot; Léo Exibard (CoRR, 2021)

A Generic Solution to Register-Bounded Synthesis with an Application to Discrete Orders. - Léo Exibard; Emmanuel Filiot; Ayrat Khalimov 001 (ICALP, 2022)

The Reactive Synthesis Competition (SYNTCOMP): 2018-2021. - Swen Jacobs; Guillermo A. Pérez 001; Remco Abraham; Véronique Bruyère; Michaël Cadilhac; Maximilien Colange; Charly Delfosse; Tom van Dijk; Alexandre Duret-Lutz; Peter Faymonville; Bernd Finkbeiner; Ayrat Khalimov 001; et al. (Int. J. Softw. Tools Technol. Transf., 2024)