Stateless model checking of the Linux kernel's hierarchical read-copy-update (tree RCU). - Michalis Kokologiannakis; Konstantinos Sagonas (SPIN, 2017)

Effective stateless model checking for C/C++ concurrency. - Michalis Kokologiannakis; Ori Lahav 001; Konstantinos Sagonas; Viktor Vafeiadis (Proc. ACM Program. Lang., 2018)

Model checking for weakly consistent libraries. - Michalis Kokologiannakis; Azalea Raad; Viktor Vafeiadis (PLDI, 2019)

Effective lock handling in stateless model checking. - Michalis Kokologiannakis; Azalea Raad; Viktor Vafeiadis (Proc. ACM Program. Lang., 2019)

Stateless model checking of the Linux kernel's read-copy update (RCU). - Michalis Kokologiannakis; Konstantinos Sagonas (Int. J. Softw. Tools Technol. Transf., 2019)

HMC: Model Checking for Hardware Memory Models. - Michalis Kokologiannakis; Viktor Vafeiadis (ASPLOS, 2020)

GenMC: A Model Checker for Weak Memory Models. - Michalis Kokologiannakis; Viktor Vafeiadis (CAV (1), 2021)

Dynamic Partial Order Reductions for Spinloops. - Michalis Kokologiannakis; Xiaowei Ren; Viktor Vafeiadis (FMCAD, 2021)

BAM: Efficient Model Checking for Barriers. - Michalis Kokologiannakis; Viktor Vafeiadis (NETYS, 2021)

PerSeVerE: persistency semantics for verification under ext4. - Michalis Kokologiannakis; Ilya Kaysin; Azalea Raad; Viktor Vafeiadis (Proc. ACM Program. Lang., 2021)

Truly stateless, optimal dynamic partial order reduction. - Michalis Kokologiannakis; Iason Marmanis; Vladimir Gladstein; Viktor Vafeiadis (Proc. ACM Program. Lang., 2022)

Model checking for a multi-execution memory model. - Evgenii Moiseenko; Michalis Kokologiannakis; Viktor Vafeiadis (Proc. ACM Program. Lang., 2022)

Unblocking Dynamic Partial Order Reduction. - Michalis Kokologiannakis; Iason Marmanis; Viktor Vafeiadis (CAV (1), 2023)

Reconciling Preemption Bounding with DPOR. - Iason Marmanis; Michalis Kokologiannakis; Viktor Vafeiadis (TACAS (1), 2023)

Kater: Automating Weak Memory Model Metatheory and Consistency Checking. - Michalis Kokologiannakis; Ori Lahav 001; Viktor Vafeiadis (Proc. ACM Program. Lang., 2023)

Extending GenMC's Usability and Performance (Replication Package). - Michalis Kokologiannakis; Rupak Majumdar; Viktor Vafeiadis (Zenodo, 2023)

Automating Memory Model Metatheory with Intersections. - Aristotelis Koutsouridis; Michalis Kokologiannakis; Viktor Vafeiadis (CONCUR, 2024)

Enhancing GenMC's Usability and Performance. - Michalis Kokologiannakis; Rupak Majumdar; Viktor Vafeiadis (TACAS (2), 2024)

Model Checking Distributed Protocols in Must. - Constantin Enea; Dimitra Giannakopoulou; Michalis Kokologiannakis; Rupak Majumdar (Proc. ACM Program. Lang., 2024)

SPORE: Combining Symmetry and Partial Order Reduction. - Michalis Kokologiannakis; Iason Marmanis; Viktor Vafeiadis (Proc. ACM Program. Lang., 2024)

Automated Reasoning under Weak Memory Consistency. - Michalis Kokologiannakis (2024)

Optimal Concolic Dynamic Partial Order Reduction. - Mohammad Hossein Khoshechin Jorshari; Michalis Kokologiannakis; Rupak Majumdar; Srinidhi Nagendra (CONCUR, 2025)

RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency. - Pavel Golovin; Michalis Kokologiannakis; Viktor Vafeiadis (Proc. ACM Program. Lang., 2025)

Dynamic Robustness Verification against Weak Memory. - Roy David Margalit; Michalis Kokologiannakis; Shachar Itzhaky; Ori Lahav 001 (Proc. ACM Program. Lang., 2025)

Model Checking C/C++ with Mixed-Size Accesses. - Iason Marmanis; Michalis Kokologiannakis; Viktor Vafeiadis (Proc. ACM Program. Lang., 2025)

Dynamic Robustness Verification Against Weak Memory (Extended Version). - Roy David Margalit; Michalis Kokologiannakis; Shachar Itzhaky; Ori Lahav 001 (CoRR, 2025)