Faculty of Science and Engineering - Research

Dr Nikolaos Tzevelekos

Nikolaos Tzevelekos

Senior Lecturer

School of Electronic Engineering and Computer Science
Queen Mary University of London

nikos.tzevelekos@qmul.ac.uk

www.qmul.ac.uk/eecs/people/profiles/tzevelekosnikos.html

Centre for Fundamental Computer Science

Research
Publications
Grants

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

solid heart icon

Publications of specific relevance to the Centre for Fundamental Computer Science

2024

An Operational Semantics for Yul
Koutavas V, Lin Y-Y and Tzevelekos N
Lecture Notes in Computer Science, Springer Nature vol. 15280, 328-346.

DOI 10.1007/978-3-031-77382-2_19

QMRO

26-11-2024

Relevant Publication

Automatic Compositional Checking of Multi-object TypeState Properties of Software
Grigore R, Distefano D and Tzevelekos N
Lecture Notes in Computer Science, Springer Nature vol. 15260, 3-40.

DOI 10.1007/978-3-031-75783-9_1

QMRO

13-11-2024

Relevant Publication

An Operational Semantics for Yul.
Koutavas V, Lin Y-Y and Tzevelekos N
SEFM. vol. 15280, 328-346. Editors: Madeira A and Knapp A.

QMRO

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.

QMRO

01-01-2024

2023

Relevant Publication

On-the-fly bisimulation equivalence checking for fresh-register automata
Bandukara MH and Tzevelekos N
Journal of Systems Architecture, Elsevier vol. 145

DOI 10.1016/j.sysarc.2023.103010

QMRO

01-12-2023

Relevant Publication

Deconstructing general references via game semantics
Tzevelekos N and Murawski AS
Samson Abramsky On Logic and Structure in Computer Science and Beyond, Springer Nature

DOI 10.1007/978-3-031-24117-8_8

QMRO

02-08-2023

Relevant Publication

Fully Abstract Normal Form Bisimulation for Call-by-Value PCF
Koutavas V, Lin Y-Y and Tzevelekos N
2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). vol. 00, 1-13.

DOI 10.1109/lics56636.2023.10175778

QMRO

29-06-2023

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.

DOI 10.1145/3531130

02-08-2022

Relevant Publication

From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
Koutavas 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.

DOI 10.1007/978-3-030-99527-0_10

QMRO

01-01-2022

Relevant Publication

On-The-Fly Bisimilarity Checking for Fresh-Register Automata
Bandukara MH and Tzevelekos N
Lecture Notes in Computer Science. vol. 13649, 187-204.

DOI 10.1007/978-3-031-21213-0_12

QMRO

01-01-2022

2021

Theorems for free from separation logic specifications
Birkedal 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.

DOI 10.1145/3473586

QMRO

19-08-2021

2020

Game Semantics for Interface Middleweight Java.
Murawski AS and Tzevelekos N
J. Acm vol. 68, 4:1-4:1.

DOI 10.1145/3428676

QMRO

11-12-2020

Symbolic execution game semantics
Lin YY and Tzevelekos N
Leibniz International Proceedings in Informatics, Lipics vol. 167

DOI 10.4230/LIPIcs.FSCD.2020.27

QMRO

01-06-2020

Bisimilarity in fresh-register automata.
Murawski AS, Ramsay SJ and Tzevelekos N
Corr vol. abs/2005.06411

QMRO

01-01-2020

Symbolic Execution Game Semantics.
Lin Y-Y and Tzevelekos N
FSCD. vol. 167, 27:1-27:1. Editors: Ariola ZM.

QMRO

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, 2019

Bulletin of Symbolic Logic, Cambridge University Press (Cup) vol. 25 (3), 420-420.

DOI 10.1017/bsl.2019.40

01-09-2019

, Open Publishing Association vol. 296 Editors: De Angelis E, Fedyukovich G, Tzevelekos N and Ulbrich M.

DOI 10.4204/eptcs.296

09-07-2019

Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
De Angelis E, Fedyukovich G, Tzevelekos N and Ulbrich M
Electronic Proceedings in Theoretical Computer Science, Open Publishing Association vol. 296

DOI 10.4204/eptcs.296.0

09-07-2019

Preface
De Angelis E, Fedyukovich G, Tzevelekos N and Ulbrich M
Electronic Proceedings in Theoretical Computer Science, EPTCS. vol. 296
09-07-2019

Higher-Order Linearisability
TZEVELEKOS NP and Murawski AS
Journal of Logical and Algebraic Methods in Programming, Elsevier

DOI 10.1016/j.jlamp.2019.01.002

QMRO

21-01-2019

DEQ: Equivalence Checker for Deterministic Register Automata
Murawski AS, Ramsay SJ and Tzevelekos N
Lecture Notes in Computer Science. vol. 11781, 350-356.

DOI 10.1007/978-3-030-31784-3_20

QMRO

01-01-2019

A Bounded Model Checking Technique for Higher-Order Programs
Lin Y-Y and Tzevelekos N
Lecture Notes in Computer Science. vol. 11951, 1-18.

DOI 10.1007/978-3-030-35540-1_1

QMRO

01-01-2019

Higher-order linearisability.
Murawski AS and Tzevelekos N
J. Log. Algebraic Methods Program. vol. 104, 86-116.

DOI 10.1016/j.jlamp.2019.01.002

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 automata
Murawski AS, Ramsay SJ and Tzevelekos N
Leibniz International Proceedings in Informatics, LIPIcs. vol. 117

DOI 10.4230/LIPIcs.MFCS.2018.72

QMRO

01-08-2018

A Trace Semantics for System F Parametric Polymorphism
JABER G and TZEVELEKOS NP
21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS).

DOI 10.1007/978-3-319-89366-2_2

QMRO

14-04-2018

Higher-Order Bounded Model Checking
Lin Y-Y and Tzevelekos N
Arxiv

QMRO

05-04-2018

2017

Algorithmic games for full ground references
TZEVELEKOS NP and Murawski AS
Formal Methods in System Design, Springer Verlag

DOI 10.1007/s10703-017-0292-9

QMRO

09-08-2017

Higher-order linearisability
Murawski AS and Tzevelekos N
Leibniz International Proceedings in Informatics, LIPIcs. vol. 85

DOI 10.4230/LIPIcs.CONCUR.2017.34

QMRO

01-08-2017

Block structure vs scope extrusion: between innocence and omniscience
Murawski AS and Tzevelekos N
Logical Methods in Computer Science, Centre Pour La Communication Scientifique Directe (Ccsd) vol. Volume 12, Issue 3

DOI 10.2168/lmcs-12(3:3)2016

27-04-2017

Reachability in Pushdown Register Automata
TZEVELEKOS NP, Murawski AS and Ramsay SJ
Journal of Computer and System Sciences

DOI 10.1016/j.jcss.2017.02.008

QMRO

08-03-2017

Trace Properties from Separation Logic Specifications
Birkedal L, Dinsdale-Young T, Jaber G, Svendsen K and Tzevelekos N

QMRO

09-02-2017

Foreword for special issue of APAL for GaLoP 2013
Hyland M, McCusker G and Tzevelekos N
Annals of Pure and Applied Logic vol. 168 (2), 233-233.

DOI 10.1016/j.apal.2016.10.004

QMRO

01-02-2017

2016

Block Structure vs. Scope Extrusion: Between Innocence and Omniscience
Murawski AS and Tzevelekos N
Logical Methods in Computer Science, Ifcolog (International Federation of Computational Logic) vol. 12 (3), 33-47.

DOI 10.1007/978-3-642-12032-9_4

QMRO

17-08-2016

Trace Semantics for Polymorphic References
Jaber G and TZEVELEKOS NP
Logic in Computer Science (LICS).

DOI 10.1145/2933575.2934509

QMRO

05-07-2016

An invitation to game semantics
Murawski AS and Tzevelekos N
Acm Siglog News, Association For Computing Machinery (Acm) vol. 3 (2), 56-67.

DOI 10.1145/2948896.2948902

31-05-2016

Nominal Game Semantics
Murawski AS and Tzevelekos N

DOI 10.1561/9781680831078

01-01-2016

2015

Bisimilarity in Fresh-Register Automata
Murawski AS, Ramsay SJ and Tzevelekos N
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science., 156-167.

DOI 10.1109/lics.2015.24

QMRO

03-08-2015

Game Semantic Analysis of Equivalence in IMJ
Murawski AS, Ramsay SJ and Tzevelekos N
Lecture Notes in Computer Science. vol. 9364, 411-428.

DOI 10.1007/978-3-319-24953-7_30

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.

DOI 10.1007/978-3-319-24953-7_19

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 Java
Murawski AS and Tzevelekos N
Acm Sigplan Notices, Association For Computing Machinery (Acm) vol. 49 (1), 517-528.

DOI 10.1145/2578855.2535880

08-01-2014

Reachability in Pushdown Register Automata
Murawski AS, Ramsay SJ and Tzevelekos N
Lecture Notes in Computer Science. vol. 8634, 464-473.

DOI 10.1007/978-3-662-44522-8_39

01-01-2014

Game Semantics for Nominal Exceptions
Murawski AS and Tzevelekos N
Lecture Notes in Computer Science. vol. 8412, 164-179.

DOI 10.1007/978-3-642-54830-7_11

01-01-2014

Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14

DOI 10.1145/2535838

01-01-2014

2013

History-Register Automata.
Tzevelekos N and Grigore R
FoSSaCS. vol. 7794, 17-33. Editors: Pfenning F.

DOI 10.2168/LMCS-12(1:7)2016

01-01-2013

Deconstructing General References via Game Semantics.
Murawski AS and Tzevelekos N
FoSSaCS. vol. 7794, 241-256. Editors: Pfenning F.

DOI 10.1007/978-3-642-37075-5_16

01-01-2013

Full abstraction for Reduced ML.
Murawski AS and Tzevelekos N
Ann. Pure Appl. Log. vol. 164, 1118-1143.

DOI 10.1016/j.apal.2013.05.007

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.

DOI 10.1007/978-3-642-38164-5_17

QMRO

01-01-2013

History-Register Automata
Tzevelekos N and Grigore R
In Foundations of Software Science and Computation Structures, Springer Nature 17-33.

DOI 10.1007/978-3-642-37075-5_2

01-01-2013

2012

Runtime Verification Based on Register Automata
Grigore R, Distefano D, Petersen RL and Tzevelekos N

DOI 10.1007/978-3-642-36742-7_19

QMRO

24-09-2012

History-Register Automata
Grigore R and Tzevelekos N
March vol. 29

DOI 10.2168/LMCS-12(1:7)2016

QMRO

04-09-2012

A System-Level Semantics
Ghica DR and Tzevelekos N

DOI 10.1016/j.entcs.2012.08.013

21-01-2012

Program equivalence in a simple language with state.
Tzevelekos N
Comput. Lang. Syst. Struct. vol. 38, 181-198.

DOI 10.1016/j.cl.2012.02.002

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.

DOI 10.1016/j.entcs.2012.08.013

01-01-2012

Runtime Verification Based on Register Automata
Distefano 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.

DOI 10.1007/978-3-642-31585-5_30

QMRO

01-01-2012

2011

Introduction to Categories and Categorical Logic
Abramsky S and Tzevelekos N
. Lecture Notes in Physics vol. 813, 3-94.

DOI 10.1007/978-3-642-12821-9_1

QMRO

07-02-2011

Fresh-Register Automata
Tzevelekos N
POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES., 295-306.

DOI 10.1145/1926385.1926420

QMRO

01-01-2011

Algorithmic Nominal Game Semantics.
Murawski AS and Tzevelekos N
ESOP. vol. 6602, 419-438. Editors: Barthe G.

DOI 10.1007/978-3-642-19718-5_22

01-01-2011

Game semantics for good general references
Murawski AS and Tzevelekos N
26TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2011)., 75-84.

DOI 10.1109/LICS.2011.31

01-01-2011

2010

Program equivalence with names
Tzevelekos N
Dagstuhl Seminar Proceedings. vol. 10351
01-01-2010

Block Structure vs. Scope Extrusion: Between Innocence and Omniscience
Murawski AS and Tzevelekos N
Lecture Notes in Computer Science. vol. 6014, 33-47.

DOI 10.1007/978-3-642-12032-9_4

01-01-2010

2009

FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES
Tzevelekos N
Log Meth Comput Sci vol. 5 (3)

DOI 10.2168/LMCS-5(3:8)2009

QMRO

01-01-2009

Full Abstraction for Reduced ML
Murawski AS and Tzevelekos N
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS. vol. 5504, 32-47. Editors: DeAlfaro L.

DOI 10.1007/978-3-642-00596-1_4

01-01-2009

Functional Reachability
Ong CHL and Tzevelekos N
24TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS., 286-295.

DOI 10.1109/LICS.2009.48

01-01-2009

2007

Full abstraction for nominal general references
Tzevelekos N
22nd Annual IEEE Symposium on Logic in Computer Science, Proceedings., 399-408.

DOI 10.1109/LICS.2007.21

01-01-2007

2006

Investigations on the dual calculus
Tzevelekos N
Theor Comput Sci vol. 360 (1-3), 289-326.

DOI 10.1016/j.tcs.2006.04.009

21-08-2006

Grants

solid heart icon

Grants of specific relevance to the Centre for Fundamental Computer Science

solid heart icon

Mokapot/Millr: Next generation cloud computing software infrastructure
Nikolaos Tzevelekos
£44,502 Innovate UK
07-05-2019 - 31-10-2019