About
I am an assistant professor at ETH Zurich. I got my PhD from MPI-SWS and my MEng from the National Technical University of Athens (NTUA).
I am broadly interested in programming languages, compilers, and software verification. More specifically, I am mainly interested in automated verification and testing, with emphasis on concurrent programming and algorithms that incorporate extensions for checking the effects of the weak memory models employed by modern microprocessors.
If you are interested in pursuing a PhD in automated verification, please email me directly.
Tools
- GenMC: a stateless model checker than can verify C/C++ programs under weak memory models
- Kater: a tool that automates weak memory model metatheory and consistency checking
Publications
You can find all my publications below (also on Google Scholar, dblp ).
-
Model Checking Distributed Protocols in Must
Constantin Enea, Dimitra Giannakopoulou, Michalis Kokologiannakis, Rupak Majumdar
OOPSLA 2024 [doi] [bib] -
Automating Memory Model Metatheory with Intersections
Aristotelis Koutsouridis, Michalis Kokologiannakis, Viktor Vafeiadis
CONCUR 2024 [doi] [bib] -
SPORE: Combining Symmetry and Partial Order Reduction
Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
PLDI 2024 [video] [doi] [bib] [project page] -
Enhancing GenMC's Usability and Performance
Michalis Kokologiannakis, Rupak Majumdar, Viktor Vafeiadis
TACAS 2024 [doi] [bib] [project page] -
Automated Reasoning under Weak Memory Consistency
Michalis Kokologiannakis
PhD Thesis [doi] [bib] -
Unblocking Dynamic Partial Order Reduction
Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
CAV 2023 [doi] [bib] [project page] -
Reconciling Preemption Bounding with DPOR
Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis
TACAS 2023 [doi] [bib] [project page] -
Kater: Automating Weak Memory Model Metatheory and Consistency Checking
Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis
POPL 2023 [video] [doi] [bib] [project page] -
Model Checking for a Multi-Execution Memory Model
Evgenii Moiseenko, Michalis Kokologiannakis, Viktor Vafeiadis
OOPSLA 2022 [video] [doi] [bib] [project page] -
Truly Stateless, Optimal Dynamic Partial Order Reduction
Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis
POPL 2022 [video] [doi] [bib] [project page] -
Dynamic Partial Order Reduction for Spinloops
Michalis Kokologiannakis, Xiaowei Ren, Viktor Vafeiadis
FMCAD 2021 [video] [doi] [bib] [project page] -
GenMC: A Model Checker for Weak Memory Models
Michalis Kokologiannakis, Viktor Vafeiadis
CAV 2021 [video] [doi] [bib] [project page] -
BAM: Efficient Model Checking for Barriers
Michalis Kokologiannakis, Viktor Vafeiadis
NETYS 2021 [video] [doi] [bib] [project page] -
PerSeVerE: Persistency Semantics for Verification under Ext4
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis
POPL 2021 [video] [doi] [bib] [project page] -
HMC: Model Checking for Hardware Memory Models
Michalis Kokologiannakis, Viktor Vafeiadis
ASPLOS 2020 [video] [doi] [bib] [project page] -
Effective Lock Handling in Stateless Model Checking
Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis
OOPSLA 2019 [video] [doi] [bib] [project page] -
Model Checking for Weakly Consistent Libraries
Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis
PLDI 2019 [video] [doi] [bib] [project page] -
Stateless model checking of the Linux kernel's read-copy update (RCU)
Michalis Kokologiannakis, Kostis Sagonas
STTT 2019 [doi] [bib] [project page] -
Effective Stateless Model Checking for C/C++ Concurrency
Michalis Kokologiannakis, Ori Lahav, Kostis Sagonas, Viktor Vafeiadis
POPL 2018 [video] [doi] [bib] [project page] -
Stateless Model Checking of the Linux Kernel's Hierarchical Read-Copy-Update (Tree RCU)
Michalis Kokologiannakis, Kostis Sagonas
SPIN 2017 [doi] [bib] [project page]
Contact
E-mail: | |
---|---|
Address: |
CNB H 104.2 Universitätstrasse 6 8092 Zürich Switzerland |