Michalis Kokologiannakis
where else to find them
no profile links on file
what they talk about
all 5 in the filters
where they keep going back
- POPL4 editions2021–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2025
on a stage with
all 12 in the filters
who talks about the same things
- Viktor Vafeiadis23 talks
- Ori Lahav17 talks
- Constantin Enea14 talks
- Iason Marmanis3 talks
- Rupak Majumdar21 talks
- Andreas Pavlogiannis18 talks
| title | conference | date |
|---|---|---|
| Dynamic Robustness Verification against Weak Memory | PLDI 2025 | 2025-06-16 |
Algorithm verifies robustness against C11/C++20 weak memory using location clocks and runs as the RSAN/Arson tool that reports full backtraces for violations… | ||
| Model Checking C/C++ with Mixed-Size Accesses | POPL 2025 | 2025-01-19 |
Presents an algorithm that lets a DPOR-based model checker handle C/C++ mixed-size accesses by treating whole instructions atomically while allowing revisits… | ||
| RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency | POPL 2025 | 2025-01-19 |
RELINCHE is a model checker that verifies per-object atomicity plus preserved synchronization under weak memory by establishing refinement between an… | ||
| Model Checking Distributed Protocols in Must | OOPSLA 2024 | 2024-10-20 |
Must is a bounded model checker that verifies real distributed implementations by instrumenting a mainstream language (example: Rust) with a tiny concurrency… | ||
| SPORE: Combining Symmetry and Partial Order Reduction | PLDI 2024 | 2024-06-24 |
SPORE is a stateless model checker that actually combines symmetry reduction and dynamic partial order reduction to cut interleavings exponentially; it proves… | ||
| Kater: Automating Weak Memory Model Metatheory and Consistency Checking | POPL 2023 | 2023-01-15 |
Kater reduces meta theoretic questions about axiomatic weak memory models to language inclusion between CAT expressions, proving decidability for a wide class… | ||
| Truly Stateless, Optimal Dynamic Partial Order Reduction | POPL 2022 | 2022-01-16 |
Claim: TruSt explores exactly one interleaving per Mazurkiewicz-equivalence class while using linear (paper shows how to get from N^2 to linear) memory instead… | ||
| PerSeVerE: Persistency Semantics for Verification under Ext4 | POPL 2021 | 2021-01-17 |
Formal semantics for ext4 are derived from the kernel implementation and stress tests and integrated with C/C++ weak-memory models; a model-checker then… | ||
| nothing matches | ||