Welcome
My name is Michalis Kokologiannakis and I am a PhD student at the Max Planck Institute for Software Systems (MPI-SWS). My advisor is Viktor Vafeiadis.
I got my MEng in Electrical and Computer Engineering from the National Technical University of Athens (NTUA) in October 2016. My diploma thesis was titled "Systematic Concurrency Testing of Read-Copy-Update under Sequentially Consistent and Weak Memory Models", and was done under the supervision of Kostis Sagonas.
Research Interests
I am broadly interested in programming languages, compilers, weak memory models, and software verification. More specifically, I am mainly interested in advancing the state of the art of testing, concurrent software verification with emphasis on systems programming, and efficient algorithms for stateless model checking that incorporate extensions for checking the effects of the weak memory models employed by modern microprocessors.
During my PhD I have been developing GenMC, a stateless model checker than can be used to verify C/C++ programs under weak memory models.
Publications
You can find all my publications below (also on Google Scholar, dblp ).
-
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: |
MPI-SWS Paul-Ehrlich-Str. 26 67663 Kaiserslautern Germany |