| 2026 | CSL | A Logic for Fresh Labelled Transition Systems. | Mohamed H. Bandukara, Nikos Tzevelekos |
| 2025 | MFCS | Register Automata with Permutations. | Mrudula Balachander, Emmanuel Filiot, Raffaella Gentilini, Nikos Tzevelekos |
| 2024 | LICS | Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence. | Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos |
| 2024 | SEFM | An Operational Semantics for Yul. | Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos |
| 2023 | LICS | Fully Abstract Normal Form Bisimulation for Call-by-Value PCF. | Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos |
| 2022 | SETTA | On-The-Fly Bisimilarity Checking for Fresh-Register Automata. | Mohamed H. Bandukara, Nikos Tzevelekos |
| 2022 | TACAS | From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques. | Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos |
| 2020 | FSCD | Symbolic Execution Game Semantics. | Yu-Yang Lin, Nikos Tzevelekos |
| 2019 | ATVA | DEQ: Equivalence Checker for Deterministic Register Automata. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2019 | SETTA | A Bounded Model Checking Technique for Higher-Order Programs. | Yu-Yang Lin, Nikos Tzevelekos |
| 2018 | FOSSACS | A Trace Semantics for System F Parametric Polymorphism. | Guilhem Jaber, Nikos Tzevelekos |
| 2018 | MFCS | Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2017 | CONCUR | Higher-Order Linearisability. | Andrzej S. Murawski, Nikos Tzevelekos |
| 2016 | LICS | Trace semantics for polymorphic references. | Guilhem Jaber, Nikos Tzevelekos |
| 2015 | ATVA | A Contextual Equivalence Checker for IMJ ∗. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2015 | ATVA | Game Semantic Analysis of Equivalence in IMJ. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2015 | LICS | Bisimilarity in Fresh-Register Automata. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2014 | FOSSACS | Game Semantics for Nominal Exceptions. | Andrzej S. Murawski, Nikos Tzevelekos |
| 2014 | MFCS | Reachability in Pushdown Register Automata. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2014 | POPL | Game semantics for interface middleweight Java. | Andrzej S. Murawski, Nikos Tzevelekos |
| 2013 | FOSSACS | Deconstructing General References via Game Semantics. | Andrzej S. Murawski, Nikos Tzevelekos |
| 2013 | FOSSACS | History-Register Automata. | Nikos Tzevelekos, Radu Grigore |
| 2013 | TACAS | Runtime Verification Based on Register Automata. | Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, Nikos Tzevelekos |
| 2012 | ICALP | Algorithmic Games for Full Ground References. | Andrzej S. Murawski, Nikos Tzevelekos |
| 2011 | ESOP | Algorithmic Nominal Game Semantics. | Andrzej S. Murawski, Nikos Tzevelekos |
| 2011 | LICS | Game Semantics for Good General References. | Andrzej S. Murawski, Nikos Tzevelekos |
| 2011 | POPL | Fresh-register automata. | Nikos Tzevelekos |
| 2010 | FOSSACS | Block Structure vs. Scope Extrusion: Between Innocence and Omniscience. | Andrzej S. Murawski, Nikos Tzevelekos |
| 2009 | FOSSACS | Full Abstraction for Reduced ML. | Andrzej S. Murawski, Nikos Tzevelekos |
| 2009 | LICS | Functional Reachability. | C.-H. Luke Ong, Nikos Tzevelekos |
| 2007 | LICS | Full abstraction for nominal general references. | Nikos Tzevelekos |