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
An Operational Semantics for YulKoutavas V, Lin Y-Y and Tzevelekos N
Lecture Notes in Computer Science, Springer Nature vol. 15280, 328-346.
26-11-2024
Automatic Compositional Checking of Multi-object TypeState Properties of SoftwareGrigore R, Distefano D and Tzevelekos N
Lecture Notes in Computer Science, Springer Nature vol. 15260, 3-40.
13-11-2024
An Operational Semantics for Yul.Koutavas V, Lin Y-Y and Tzevelekos N
SEFM. vol. 15280, 328-346. Editors: Madeira A and Knapp A.
01-01-2024
Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence.Koutavas V, Lin Y-Y and Tzevelekos N
LICS., 53:1-53:1. Editors: Sobocinski P, Lago UD and Esparza J.
01-01-2024
2023
On-the-fly bisimulation equivalence checking for fresh-register automataBandukara MH and Tzevelekos N
Journal of Systems Architecture, Elsevier vol. 145
01-12-2023
Deconstructing general references via game semanticsTzevelekos N and Murawski AS
Samson Abramsky on Logic and Structure in Computer Science and Beyond, Springer Nature
02-08-2023
Fully Abstract Normal Form Bisimulation for Call-by-Value PCFKoutavas V, Lin Y-Y and Tzevelekos N
2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). vol. 00, 1-13.
29-06-2023
2022
Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer ScienceLICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science.
02-08-2022
From Bounded Checking to Verification of Equivalence via Symbolic Up-to TechniquesKoutavas V, Lin YY and Tzevelekos N
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 13244 LNCS, 178-195.
01-01-2022
On-The-Fly Bisimilarity Checking for Fresh-Register AutomataBandukara MH and Tzevelekos N
Lecture Notes in Computer Science. vol. 13649, 187-204.
01-01-2022
2021
Theorems for free from separation logic specificationsBirkedal L, Dinsdale-Young T, Guéneau A, Jaber G, Svendsen K and Tzevelekos N
Proceedings of the ACM on Programming Languages. vol. 5 (ICFP), 1-29.
19-08-2021
2020
Game Semantics for Interface Middleweight Java.Murawski AS and Tzevelekos N
J. Acm vol. 68, 4:1-4:1.
11-12-2020
Symbolic execution game semanticsLin YY and Tzevelekos N
Leibniz International Proceedings in Informatics, Lipics vol. 167
01-06-2020
Bisimilarity in fresh-register automata.Murawski AS, Ramsay SJ and Tzevelekos N
Corr vol. abs/2005.06411
01-01-2020
Symbolic Execution Game Semantics.Lin Y-Y and Tzevelekos N
FSCD. vol. 167, 27:1-27:1. Editors: Ariola ZM.
01-01-2020
2019
12TH PANHELLENIC LOGIC SYMPOSIUM (PLS 12, 2019) CO-SPONSORED BY THE ASSOCIATION FOR SYMBOLIC LOGIC Anogeia, Crete, Greece June 26–30, 2019Bulletin of Symbolic Logic, Cambridge University Press (Cup) vol. 25 (3), 420-420.
01-09-2019
, Open Publishing Association vol. 296 Editors: De Angelis E, Fedyukovich G, Tzevelekos N and Ulbrich M.
09-07-2019
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational ReasoningDe Angelis E, Fedyukovich G, Tzevelekos N and Ulbrich M
Electronic Proceedings in Theoretical Computer Science, Open Publishing Association vol. 296
09-07-2019
PrefaceDe Angelis E, Fedyukovich G, Tzevelekos N and Ulbrich M
Electronic Proceedings in Theoretical Computer Science, EPTCS. vol. 296
09-07-2019
Higher-Order LinearisabilityTZEVELEKOS NP and Murawski AS
Journal of Logical and Algebraic Methods in Programming, Elsevier
21-01-2019
DEQ: Equivalence Checker for Deterministic Register AutomataMurawski AS, Ramsay SJ and Tzevelekos N
Lecture Notes in Computer Science. vol. 11781, 350-356.
01-01-2019
A Bounded Model Checking Technique for Higher-Order ProgramsLin Y-Y and Tzevelekos N
Lecture Notes in Computer Science. vol. 11951, 1-18.
01-01-2019
Higher-order linearisability.Murawski AS and Tzevelekos N
J. Log. Algebraic Methods Program. vol. 104, 86-116.
01-01-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.HCVS/PERR@ETAPS. vol. 296 Editors: Angelis ED, Fedyukovich G, Tzevelekos N and Ulbrich M.
01-01-2019
2018
Polynomial-time equivalence testing for deterministic fresh-register automataMurawski AS, Ramsay SJ and Tzevelekos N
Leibniz International Proceedings in Informatics, LIPIcs. vol. 117
01-08-2018
A Trace Semantics for System F Parametric PolymorphismJABER G and TZEVELEKOS NP
21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
14-04-2018
2017
Algorithmic games for full ground referencesTZEVELEKOS NP and Murawski AS
Formal Methods in System Design, Springer Verlag
09-08-2017
Higher-order linearisabilityMurawski AS and Tzevelekos N
Leibniz International Proceedings in Informatics, LIPIcs. vol. 85
01-08-2017
Block structure vs scope extrusion: between innocence and omniscienceMurawski AS and Tzevelekos N
Logical Methods in Computer Science, Centre Pour La Communication Scientifique Directe (Ccsd) vol. Volume 12, Issue 3
27-04-2017
Reachability in Pushdown Register AutomataTZEVELEKOS NP, Murawski AS and Ramsay SJ
Journal of Computer and System Sciences
08-03-2017
Trace Properties from Separation Logic SpecificationsBirkedal L, Dinsdale-Young T, Jaber G, Svendsen K and Tzevelekos N
09-02-2017
Foreword for special issue of APAL for GaLoP 2013Hyland M, McCusker G and Tzevelekos N
Annals of Pure and Applied Logic vol. 168 (2), 233-233.
01-02-2017
2016
Block Structure vs. Scope Extrusion: Between Innocence and OmniscienceMurawski AS and Tzevelekos N
Logical Methods in Computer Science, Ifcolog (International Federation of Computational Logic) vol. 12 (3), 33-47.
17-08-2016
Trace Semantics for Polymorphic ReferencesJaber G and TZEVELEKOS NP
Logic in Computer Science (LICS).
05-07-2016
An invitation to game semanticsMurawski AS and Tzevelekos N
Acm Siglog News, Association For Computing Machinery (Acm) vol. 3 (2), 56-67.
31-05-2016
2015
Bisimilarity in Fresh-Register AutomataMurawski AS, Ramsay SJ and Tzevelekos N
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science., 156-167.
03-08-2015
Game Semantic Analysis of Equivalence in IMJMurawski AS, Ramsay SJ and Tzevelekos N
Lecture Notes in Computer Science. vol. 9364, 411-428.
01-01-2015
A Contextual Equivalence Checker for IMJ*Murawski AS, Ramsay SJ and Tzevelekos N
Lecture Notes in Computer Science. vol. 9364, 234-240.
01-01-2015
Semantics and Verification of Object-Oriented Languages (NII Shonan Meeting 2015-13).Igarashi A, Murawski AS and Tzevelekos N
Nii Shonan Meet. Rep. vol. 2015
01-01-2015
2014
Game semantics for interface middleweight JavaMurawski AS and Tzevelekos N
Acm Sigplan Notices, Association For Computing Machinery (Acm) vol. 49 (1), 517-528.
08-01-2014
Reachability in Pushdown Register AutomataMurawski AS, Ramsay SJ and Tzevelekos N
Lecture Notes in Computer Science. vol. 8634, 464-473.
01-01-2014
Game Semantics for Nominal ExceptionsMurawski AS and Tzevelekos N
Lecture Notes in Computer Science. vol. 8412, 164-179.
01-01-2014
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '1401-01-2014
2013
History-Register Automata.Tzevelekos N and Grigore R
FoSSaCS. vol. 7794, 17-33. Editors: Pfenning F.
01-01-2013
Deconstructing General References via Game Semantics.Murawski AS and Tzevelekos N
FoSSaCS. vol. 7794, 241-256. Editors: Pfenning F.
01-01-2013
Full abstraction for Reduced ML.Murawski AS and Tzevelekos N
Ann. Pure Appl. Log. vol. 164, 1118-1143.
01-01-2013
Towards Nominal Abramsky.Murawski AS and Tzevelekos N
Computation, Logic, Games, and Quantum Foundations. vol. 7860, 246-263. Editors: Coecke B, Ong L and Panangaden P.
01-01-2013
History-Register AutomataTzevelekos N and Grigore R
In Foundations of Software Science and Computation Structures, Springer Nature 17-33.
01-01-2013
2012
Runtime Verification Based on Register AutomataGrigore R, Distefano D, Petersen RL and Tzevelekos N
24-09-2012
Program equivalence in a simple language with state.Tzevelekos N
Comput. Lang. Syst. Struct. vol. 38, 181-198.
01-01-2012
A System-Level Game Semantics.Ghica DR and Tzevelekos N
Mfps, Elsevier vol. 286, 191-211. Editors: Berger U and Mislove MW.
01-01-2012
Runtime Verification Based on Register AutomataDistefano D, Grigore R, Petersen RL and Tzevelekos N
Corr vol. abs/1209.5325
01-01-2012
Algorithmic Games for Full Ground References.Murawski AS and Tzevelekos N
Icalp (2), Springer vol. 7392, 312-324. Editors: Czumaj A, Mehlhorn K, Pitts AM and Wattenhofer R.
01-01-2012
2011
Introduction to Categories and Categorical LogicAbramsky S and Tzevelekos N
. Lecture Notes in Physics vol. 813, 3-94.
07-02-2011
Fresh-Register AutomataTzevelekos N
POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES., 295-306.
01-01-2011
Algorithmic Nominal Game Semantics.Murawski AS and Tzevelekos N
ESOP. vol. 6602, 419-438. Editors: Barthe G.
01-01-2011
Game semantics for good general referencesMurawski AS and Tzevelekos N
26TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2011)., 75-84.
01-01-2011
2010
Block Structure vs. Scope Extrusion: Between Innocence and OmniscienceMurawski AS and Tzevelekos N
Lecture Notes in Computer Science. vol. 6014, 33-47.
01-01-2010
2009
FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCESTzevelekos N
Log Meth Comput Sci vol. 5 (3)
01-01-2009
Full Abstraction for Reduced MLMurawski AS and Tzevelekos N
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS. vol. 5504, 32-47. Editors: DeAlfaro L.
01-01-2009
Functional ReachabilityOng CHL and Tzevelekos N
24TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS., 286-295.
01-01-2009
2007
Full abstraction for nominal general referencesTzevelekos N
22nd Annual IEEE Symposium on Logic in Computer Science, Proceedings., 399-408.
01-01-2007
2006
Investigations on the dual calculusTzevelekos N
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