Dr Nikolaos Tzevelekos
Senior Lecturer
School of Electronic Engineering and Computer Science
Queen Mary University of London
Queen Mary University of London
Research
Program analysis, Game semantics, Denotational semantics, Automata over infinite alphabets
Interests
My focus is on Theoretical Computer Science and in particular I study the mathematical meaning of computation. I devise mathematical models of programming languages, expressed in game semantics at the concrete level and in category theory at the abstract level. Moreover, I examine applications of these models to program analysis in order to develop methods and tools for formally analysing and checking software.Publications
Publications of specific relevance to the Centre for Fundamental Computer Science2024
Koutavas V, Lin Y-Y and Tzevelekos N (2024). An Operational Semantics for Yul. Lecture Notes in Computer Science, Springer Nature vol. 15280, 328-346. 26-11-2024
Grigore R, Distefano D and Tzevelekos N (2024). Automatic Compositional Checking of Multi-object TypeState Properties of Software. Lecture Notes in Computer Science, Springer Nature vol. 15260, 3-40. 13-11-2024
Koutavas V, Lin Y-Y and Tzevelekos N (2024). An Operational Semantics for Yul., Editors: Madeira A and Knapp A. 01-01-2024
Koutavas V, Lin Y-Y and Tzevelekos N (2024). Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence., Editors: Sobocinski P, Lago UD and Esparza J. 01-01-2024
2023
Bandukara MH and Tzevelekos N (2023). On-the-fly bisimulation equivalence checking for fresh-register automata. Journal of Systems Architecture, Elsevier vol. 145 01-12-2023
Tzevelekos N and Murawski AS (2023). Deconstructing general references via game semantics. Samson Abramsky on Logic and Structure in Computer Science and Beyond, Springer Nature 02-08-2023
Koutavas V, Lin Y-Y and Tzevelekos N (2023). Fully Abstract Normal Form Bisimulation for Call-by-Value PCF. 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). 29-06-2023
2022
(2022). Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science. 02-08-2022
Koutavas V, Lin YY and Tzevelekos N (2022). From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques. 01-01-2022
Bandukara MH and Tzevelekos N (2022). On-The-Fly Bisimilarity Checking for Fresh-Register Automata. 01-01-2022
2021
Birkedal L, Dinsdale-Young T, Guéneau A, Jaber G, Svendsen K and Tzevelekos N (2021). Theorems for free from separation logic specifications. 19-08-2021
2020
Murawski AS and Tzevelekos N (2020). Game Semantics for Interface Middleweight Java. J. ACM vol. 68, 4:1-4:1. 11-12-2020
Lin YY and Tzevelekos N (2020). Symbolic execution game semantics. Leibniz International Proceedings in Informatics, LIPIcs vol. 167 01-06-2020
Murawski AS, Ramsay SJ and Tzevelekos N (2020). Bisimilarity in fresh-register automata. CoRR vol. abs/2005.06411 01-01-2020
2019
(2019). 12TH PANHELLENIC LOGIC SYMPOSIUM (PLS 12, 2019) CO-SPONSORED BY THE ASSOCIATION FOR SYMBOLIC LOGIC Anogeia, Crete, Greece June 26–30, 2019. Bulletin of Symbolic Logic, Cambridge University Press (CUP) vol. 25 (3), 420-420. 01-09-2019
(2019). ., Editors: De Angelis E, Fedyukovich G, Tzevelekos N and Ulbrich M. 09-07-2019
De Angelis E, Fedyukovich G, Tzevelekos N and Ulbrich M (2019). Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning. Electronic Proceedings in Theoretical Computer Science, Open Publishing Association vol. 296 09-07-2019
TZEVELEKOS NP and Murawski AS (2019). Higher-Order Linearisability. Journal of Logical and Algebraic Methods in Programming, Elsevier 21-01-2019
Murawski AS, Ramsay SJ and Tzevelekos N (2019). DEQ: Equivalence Checker for Deterministic Register Automata. 01-01-2019
Lin Y-Y and Tzevelekos N (2019). A Bounded Model Checking Technique for Higher-Order Programs. 01-01-2019
Murawski AS and Tzevelekos N (2019). Higher-order linearisability. J. Log. Algebraic Methods Program. vol. 104, 86-116. 01-01-2019
(2019). Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning, HCVS/PERR@ETAPS 2019, Prague, Czech Republic, 6-7th April 2019., Editors: Angelis ED, Fedyukovich G, Tzevelekos N and Ulbrich M. 01-01-2019
2018
Murawski AS, Ramsay SJ and Tzevelekos N (2018). Polynomial-time equivalence testing for deterministic fresh-register automata. 01-08-2018
JABER G and TZEVELEKOS NP (2018). A Trace Semantics for System F Parametric Polymorphism. 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). 14-04-2018
2017
TZEVELEKOS NP and Murawski AS (2017). Algorithmic games for full ground references. Formal Methods in System Design, Springer Verlag 09-08-2017
Murawski AS and Tzevelekos N (2017). Block structure vs scope extrusion: between innocence and omniscience. Logical Methods in Computer Science, Centre pour la Communication Scientifique Directe (CCSD) vol. Volume 12, Issue 3 27-04-2017
TZEVELEKOS NP, Murawski AS and Ramsay SJ (2017). Reachability in Pushdown Register Automata. Journal of Computer and System Sciences 08-03-2017
Birkedal L, Dinsdale-Young T, Jaber G, Svendsen K and Tzevelekos N (2017). Trace Properties from Separation Logic Specifications. 09-02-2017
Hyland M, McCusker G and Tzevelekos N (2017). Foreword for special issue of APAL for GaLoP 2013. ANNALS OF PURE AND APPLIED LOGIC vol. 168 (2), 233-233. 01-02-2017
2016
Murawski AS and Tzevelekos N (2016). Block Structure vs. Scope Extrusion: Between Innocence and Omniscience. Logical Methods in Computer Science, IfCoLog (International Federation of Computational Logic) vol. 12 (3), 33-47. 17-08-2016
Jaber G and TZEVELEKOS NP (2016). Trace Semantics for Polymorphic References. Logic in Computer Science (LICS). 05-07-2016
Murawski AS and Tzevelekos N (2016). An invitation to game semantics. ACM SIGLOG News, Association for Computing Machinery (ACM) vol. 3 (2), 56-67. 31-05-2016
2015
Murawski AS, Ramsay SJ and Tzevelekos N (2015). Bisimilarity in Fresh-Register Automata. 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. 03-08-2015
Murawski AS, Ramsay SJ and Tzevelekos N (2015). Game Semantic Analysis of Equivalence in IMJ. 01-01-2015
Murawski AS, Ramsay SJ and Tzevelekos N (2015). A Contextual Equivalence Checker for IMJ*. 01-01-2015
Igarashi A, Murawski AS and Tzevelekos N (2015). Semantics and Verification of Object-Oriented Languages (NII Shonan Meeting 2015-13). NII Shonan Meet. Rep. vol. 2015 01-01-2015
2014
Murawski AS and Tzevelekos N (2014). Game semantics for interface middleweight Java. ACM SIGPLAN Notices, Association for Computing Machinery (ACM) vol. 49 (1), 517-528. 08-01-2014
Murawski AS, Ramsay SJ and Tzevelekos N (2014). Reachability in Pushdown Register Automata. 01-01-2014
(2014). Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14. 01-01-2014
2013
Murawski AS and Tzevelekos N (2013). Deconstructing General References via Game Semantics., Editors: Pfenning F. 01-01-2013
Murawski AS and Tzevelekos N (2013). Full abstraction for Reduced ML. Ann. Pure Appl. Log. vol. 164, 1118-1143. 01-01-2013
Murawski AS and Tzevelekos N (2013). Towards Nominal Abramsky., Editors: Coecke B, Ong L and Panangaden P. 01-01-2013
Tzevelekos N and Grigore R (2013). History-Register Automata. Foundations of Software Science and Computation Structures 17-33. 01-01-2013
2012
Grigore R, Distefano D, Petersen RL and Tzevelekos N (2012). Runtime Verification Based on Register Automata. 24-09-2012
Tzevelekos N (2012). Program equivalence in a simple language with state. Comput. Lang. Syst. Struct. vol. 38, 181-198. 01-01-2012
Ghica DR and Tzevelekos N (2012). A System-Level Game Semantics., Editors: Berger U and Mislove MW. MFPS, Elsevier vol. 286, 191-211. 01-01-2012
Distefano D, Grigore R, Petersen RL and Tzevelekos N (2012). Runtime Verification Based on Register Automata. CoRR vol. abs/1209.5325 01-01-2012
Murawski AS and Tzevelekos N (2012). Algorithmic Games for Full Ground References., Editors: Czumaj A, Mehlhorn K, Pitts AM and Wattenhofer R. ICALP (2), Springer vol. 7392, 312-324. 01-01-2012
2011
Abramsky S and Tzevelekos N (2011). Introduction to Categories and Categorical Logic. . Lecture Notes in
Physics vol. 813, 3-94. 07-02-2011
Murawski AS and Tzevelekos N (2011). Algorithmic Nominal Game Semantics., Editors: Barthe G. 01-01-2011
2010
Murawski AS and Tzevelekos N (2010). Block Structure vs. Scope Extrusion: Between Innocence and Omniscience. 01-01-2010
2009
Tzevelekos N (2009). FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES. LOG METH COMPUT SCI vol. 5 (3) 01-01-2009
Murawski AS and Tzevelekos N (2009). Full Abstraction for Reduced ML., Editors: DeAlfaro L. 01-01-2009
2007
2006
Tzevelekos N (2006). Investigations on the dual calculus. THEOR COMPUT SCI vol. 360 (1-3), 289-326. 21-08-2006
Grants
Grants of specific relevance to the Centre for Fundamental Computer ScienceMokapot/Millr: Next generation cloud computing software infrastructureNikolaos Tzevelekos
£44,502 Innovate UK (07-05-2019 - 31-10-2019)