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 Fundamentals of AI and Computational Theory2025
A Logic For Fresh Labelled Transition SystemsBandukara MH Tzevelekos N
In Arxiv
17-06-2025
Bisimilarity in fresh-register automataMurawski AS Ramsay SJ
Logical Methods in Computer Science, Centre Pour La Communication Scientifique Directe (Ccsd) vol. Volume 21, Issue 1
06-02-2025
2024
An Operational Semantics for YulKoutavas V Lin Y-Y
Lecture Notes in Computer Science, Springer Nature vol. 15280, 328-346.
26-11-2024
An Operational Semantics for YulKoutavas V Lin Y-Y Tzevelekos N
In Arxiv
01-07-2024
2023
Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program EquivalenceKoutavas V Lin Y-Y Tzevelekos N
In Arxiv
02-11-2023
Fully Abstract Normal Form Bisimulation for Call-by-Value PCFKoutavas V Lin Y-Y Tzevelekos N
In Arxiv
02-10-2023
Deconstructing general references via game semanticsTzevelekos N
Samson Abramsky on Logic and Structure in Computer Science and Beyond, Springer Nature
02-08-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
2021
From Bounded Checking to Verification of Equivalence via Symbolic Up-to TechniquesKoutavas V Lin Y-Y Tzevelekos N
In Arxiv
06-05-2021
2020
Game Semantics for Interface Middleweight Java.Murawski AS
J. Acm vol. 68, 4:1-4:1.
11-12-2020
Symbolic execution game semanticsLin YY Tzevelekos N
Leibniz International Proceedings in Informatics Lipics vol. 167
01-06-2020
Bisimilarity in fresh-register automataMurawski AS Ramsay SJ Tzevelekos N
In Arxiv
13-05-2020
Symbolic Execution Game SemanticsLin Y-Y Tzevelekos N
In Arxiv
20-02-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
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
Electronic Proceedings in Theoretical Computer Science, Open Publishing Association vol. 296
09-07-2019
PrefaceDe Angelis E Fedyukovich G Ulbrich M
Electronic Proceedings in Theoretical Computer Science Eptcs. vol. 296
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
In Arxiv
08-07-2019
Higher-Order LinearisabilityTZEVELEKOS NP
Journal of Logical and Algebraic Methods in Programming, Elsevier
21-01-2019
Higher-order linearisability.Murawski AS 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
01-01-2019
2018
A Trace Semantics for System F Parametric PolymorphismJABER G TZEVELEKOS NP
21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
14-04-2018
Higher-Order Bounded Model CheckingLin Y-Y Tzevelekos N
In Arxiv
05-04-2018
2017
Algorithmic games for full ground referencesTZEVELEKOS NP Murawski AS
Formal Methods in System Design, Springer Verlag
09-08-2017
Block structure vs scope extrusion: between innocence and omniscienceMurawski AS
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 Ramsay SJ
Journal of Computer and System Sciences
08-03-2017
Trace Properties from Separation Logic SpecificationsBirkedal L Dinsdale-Young T Svendsen K
In Arxiv
09-02-2017
Foreword for special issue of APAL for GaLoP 2013Hyland M McCusker G Tzevelekos N
Annals of Pure and Applied Logic vol. 168 (2), 233-233.
01-02-2017
2016
Higher-Order LinearisabilityMurawski AS Tzevelekos N
In Arxiv
25-10-2016
Block Structure vs. Scope Extrusion: Between Innocence and OmniscienceMurawski AS
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 TZEVELEKOS NP
Logic in Computer Science (LICS).
05-07-2016
An invitation to game semanticsMurawski AS Tzevelekos N
Acm Siglog News, Association For Computing Machinery (Acm) vol. 3 (2), 56-67.
31-05-2016
Block structure vs scope extrusion: between innocence and omniscienceMurawski AS Tzevelekos N
In Arxiv
08-05-2016
2015
Bisimilarity in Fresh-Register AutomataMurawski AS Ramsay SJ 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 Tzevelekos N
Lecture Notes in Computer Science. vol. 9364, 411-428.
01-01-2015
A Contextual Equivalence Checker for IMJ*Murawski AS Ramsay SJ
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
Nii Shonan Meet. Rep. vol. 2015
01-01-2015
2014
Game semantics for interface middleweight JavaMurawski AS
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages., 517-528.
08-01-2014
Reachability in Pushdown Register AutomataMurawski AS Ramsay SJ Tzevelekos N
Lecture Notes in Computer Science. vol. 8634, 464-473.
01-01-2014
Game Semantics for Nominal ExceptionsMurawski AS 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 Grigore R Pfenning F
FoSSaCS. vol. 7794, 17-33.
01-01-2013
Deconstructing General References via Game Semantics.Murawski AS Pfenning F
FoSSaCS. vol. 7794, 241-256.
01-01-2013
Full abstraction for Reduced ML.Murawski AS Tzevelekos N
Ann. Pure Appl. Log. vol. 164, 1118-1143.
01-01-2013
Towards Nominal Abramsky.Murawski AS Tzevelekos N Coecke B Ong L Panangaden P
Computation, Logic, Games, and Quantum Foundations. vol. 7860, 246-263.
01-01-2013
History-Register AutomataTzevelekos N
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 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 Tzevelekos N Berger U Mislove MW
Mfps, Elsevier vol. 286, 191-211.
01-01-2012
Runtime Verification Based on Register AutomataDistefano D Grigore R Petersen RL
Corr vol. abs/1209.5325
01-01-2012
Algorithmic Games for Full Ground References.Murawski AS Tzevelekos N Czumaj A Mehlhorn K Pitts AM Wattenhofer R
Icalp (2), Springer vol. 7392, 312-324.
01-01-2012
2011
Introduction to Categories and Categorical LogicAbramsky S
In Arxiv
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 Tzevelekos N Barthe G
ESOP. vol. 6602, 419-438.
01-01-2011
Game semantics for good general referencesMurawski AS
26TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2011)., 75-84.
01-01-2011
2010
Program equivalence with namesTzevelekos N
Dagstuhl Seminar Proceedings. vol. 10351
01-01-2010
Block Structure vs. Scope Extrusion: Between Innocence and OmniscienceMurawski AS
Lecture Notes in Computer Science. vol. 6014, 33-47.
01-01-2010
2009
Full abstraction for nominal general referencesTzevelekos N
In Arxiv
26-07-2009
FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCESTzevelekos N
Log Meth Comput Sci vol. 5 (3)
01-01-2009
Full Abstraction for Reduced MLMurawski AS Tzevelekos N DeAlfaro L
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS. vol. 5504, 32-47.
01-01-2009
Functional ReachabilityOng CHL 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
An Operational Semantics for YulKoutavas V Lin Y-Y Tzevelekos N
22nd International Conference on Software Engineering and Formal Methods.
Register Automata with PermutationsBalachander M Filiot E Gentilini R Tzevelekos N
2025 International Symposium on Mathematical Foundations of Computer Science.
Home PageTzevelekos N
Fully Abstract Normal Form Bisimulation for Call-by-Value PCFKoutavas V Lin Y-Y Tzevelekos N
Journal of The Acm, Association For Computing Machinery (Acm)
Higher-Order LinearisabilityTZEVELEKOS NP Murawski AS
28th International Conference on Concurrency Theory.
Polynomial-time equivalence testing for deterministic fresh-register automataTZEVELEKOS NP Murawski AS Ramsay SJ
Mathematical Foundations of Computer Science.
DEQ : Equivalence Checker for Deterministic Register AutomataTzevelekos N Murawski AM Ramsay S
ATVA 2019: International Symposium on Automated Technology for Verification and Analysis.
A Bounded Model Checking Technique for Higher-Order ProgramsTzevelekos N Lin Y-Y
SETTA 2019 Symposium on Dependable Software Engineering Theories, Tools and Applications.
Symbolic Execution Game SemanticsTzevelekos N Lin Y-Y
International Conference on Formal Structures for Computation and Deduction.
Theorems for Free from Separation Logic SpecificationsTzevelekos N Jaber G Birkedal L DINSDALE-YOUNG T GUÉNEAU A SVENDSEN K
26th ACM SIGPLAN International Conference on Functional Programming.
From Bounded Checking to Verification of Equivalence via Symbolic Up-to TechniquesKoutavas V Lin Y-Y Tzevelekos N
28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
On-the-Fly Bisimilarity Checking for Fresh-Register AutomataBandukara H Tzevelekos N
Symposium on dependable software engineering (SETTA'22).
On-The-Fly Bisimulation Equivalence Checking for Fresh-Register AutomataTzevelekos N Bandukara MH
The Journal of Systems Architecture: Embedded Software Design, Elsevier
Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program EquivalenceKoutavas V Lin Y-Y Tzevelekos N
2024 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
Automatic Compositional Checking of Multi-Object TypeState Properties of SoftwareGrigore R Distefano D Tzevelekos N
Principles of Verification: Cycling The Probabilistic Landscape
Grants
Grants of specific relevance to the Centre for Fundamentals of AI and Computational TheoryMokapot/Millr: Next generation cloud computing software infrastructureNikolaos Tzevelekos
£44,502 Innovate UK
07-05-2019 - 31-10-2019
Research Group
PhD Students
- Niki Omidvari
Theory
News
No news items found.