Dr Nikos Tzevelekos

Teaching

Algorithms and Data Structures (Undergraduate)

The module is an introduction to Algorithms and Data Structures. It covers topics such as running time of algorithms, asymptotic complexity, simple and advanced sorting algorithms, divide and conquer algorithms, recursion, dynamic programming, greedy algorithms, basic data structures (strings, arrays, lists), linked lists, trees, hash tables.

Automata and Formal Languages (Undergraduate)

Automata and formal languages are fundamental concepts in Computer Science. Automata are abstract machines that are used for representing computational processes in a mathematically precise fashion. Moreover, any device interacting with the outside world, whether a simple program or a complex system, requires well-defined, formal input and output languages. We will study automata and their relationship with formal languages and grammars.

Program Specifications (Postgraduate/Undergraduate)

The module will cover: 1. Introduction to Logic for Systems and Program Verification and Analysis 2. Using Hoare Logic: The specification language - describing properties of programs; Proof rules in Hoare logic - verifying properties of programs; Basic technologies behind building automatic program verification tools based on Hoare logic; Using automatic verification tools based on Hoare logic. 3. Introduction to modelchecking and Spin: Temporal logic: modelling states and operations of a system; Modelchecking logics in particular CTL; Safety and Liveness in systems; Using Spin for checking properties and for problem solving.

Research

Research Interests:

I am a Senior Lecturer in Computer Science. 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.

Themes:
- Program analysis
- Game semantics
- Denotational semantics
- Automata over infinite alphabets

Publications

(publicationYear). title. nameOfConference

DOI: 10.4204/eptcs.296

QMRO: qmroHref

Citations: 0
Murawski AS, Tzevelekos N (2019). Higher-order linearisability. nameOfConference

DOI: 10.1016/j.jlamp.2019.01.002

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/55025

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

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

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/36555

Citations: 0
Lin Y-Y, Tzevelekos N (2018). Higher-Order Bounded Model Checking. nameOfConference

DOI: doi

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/42063

Citations: 0
Murawski AS, Ramsay SJ, Tzevelekos N (2018). Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata.. nameOfConference

DOI: doi

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/44616

Citations: 0
TZEVELEKOS NP, Murawski AS (2017). Algorithmic games for full ground references. nameOfConference

DOI: 10.1007/s10703-017-0292-9

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/25859

Citations: 0
TZEVELEKOS NP, Murawski AS, Ramsay SJ (2017). Reachability in Pushdown Register Automata. nameOfConference

DOI: 10.1016/j.jcss.2017.02.008

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/21819

Citations: 0
Hyland M, McCusker G, Tzevelekos N (2017). Foreword for special issue of APAL for GaLoP 2013. nameOfConference

DOI: 10.1016/j.apal.2016.10.004

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/25576

Citations: 0
Murawski AS, Tzevelekos N (2017). Higher-Order Linearisability.. nameOfConference

DOI: doi

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/25012

Citations: 0
Murawski AS, Tzevelekos N (2016). Block Structure vs. Scope Extrusion: Between Innocence and Omniscience. nameOfConference

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

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/13737

Citations: 0
Jaber G, TZEVELEKOS NP (2016). Trace Semantics for Polymorphic References. Logic in Computer Science (LICS)

DOI: 10.1145/2933575.2934509

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/13081

Citations: 0
TZEVELEKOS NP, Grigore R (2016). History-Register Automata. nameOfConference

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

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/12585

Citations: 0
Murawski AS, Tzevelekos N (2016). An invitation to game semantics.. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 0
Murawski AS, Tzevelekos N (2016). BLOCK STRUCTURE VS SCOPE EXTRUSION: BETWEEN INNOCENCE AND OMNISCIENCE. nameOfConference

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

QMRO: qmroHref

Citations: 0
Murawski AS, Tzevelekos N (2016). Nominal Game Semantics. nameOfConference

DOI: 10.1561/2500000017

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/14878

Citations: 0
Murawski AS, Ramsay SJ, Tzevelekos N (2015). A Contextual Equivalence Checker for IMJ. nameOfConference

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

QMRO: qmroHref

Citations: 2
Murawski AS, Ramsay SJ, Tzevelekos N et al. (2015). Bisimilarity in Fresh-Register Automata. nameOfConference

DOI: 10.1109/LICS.2015.24

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/13504

Citations: 2
Murawski AS, Ramsay SJ, Tzevelekos N (2015). Game Semantic Analysis of Equivalence in IMJ. nameOfConference

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

QMRO: qmroHref

Citations: 4
Igarashi A, Murawski AS, Tzevelekos N (2015). Semantics and Verification of Object-Oriented Languages (NII Shonan Meeting 2015-13).. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 0
Murawski AS, Tzevelekos N (2014). Game Semantics for Interface Middleweight Java. nameOfConference

DOI: 10.1145/2535838

QMRO: qmroHref

Citations: 4
Murawski AS, Tzevelekos N (2014). Game Semantics for Nominal Exceptions.. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 0
Murawski AS, Tzevelekos N (2014). Game semantics for interface middleweight Java.. nameOfConference

DOI: doi

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/23397

Citations: 0
Murawski AS, Ramsay SJ, Tzevelekos N (2014). Reachability in Pushdown Register Automata. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 3
Murawski AS, Tzevelekos N (2013). Deconstructing General References via Game Semantics.. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 0
Murawski AS, Tzevelekos N (2013). Full abstraction for Reduced ML.. nameOfConference

DOI: 10.1016/j.apal.2013.05.007

QMRO: qmroHref

Citations: 0
Tzevelekos N, Grigore R (2013). History-Register Automata.. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 0
Grigore R, Distefano D, Petersen RL et al. (2013). Runtime Verification Based on Register Automata. nameOfConference

DOI: doi

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/19031

Citations: 0
Murawski AS, Tzevelekos N (2013). Towards Nominal Abramsky.. nameOfConference

DOI: doi

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/5321

Citations: 0
Ghica DR, Tzevelekos N (2012). A System-Level Game Semantics.. nameOfConference

DOI: 10.1016/j.entcs.2012.08.013

QMRO: qmroHref

Citations: 0
Ghica DR, Tzevelekos N (2012). A System-Level Semantics. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 0
Murawski AS, Tzevelekos N (2012). Algorithmic Games for Full Ground References.. nameOfConference

DOI: doi

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/25577

Citations: 0
Tzevelekos N (2012). Program equivalence in a simple language with state.. nameOfConference

DOI: 10.1016/j.cl.2012.02.002

QMRO: qmroHref

Citations: 0
Distefano D, Grigore R, Petersen RL et al. (2012). Runtime Verification Based on Register Automata. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 0
Murawski AS, Tzevelekos N (2011). Algorithmic Nominal Game Semantics.. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 0
Tzevelekos N (2011). Fresh-Register Automata. nameOfConference

DOI: 10.1145/1926385.1926420

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/7651

Citations: 0
Murawski AS, Tzevelekos N, IEEE (2011). Game semantics for good general references. nameOfConference

DOI: 10.1109/LICS.2011.31

QMRO: qmroHref

Citations: 9
Murawski AS, Tzevelekos N (2010). Block Structure vs. Scope Extrusion: Between Innocence and Omniscience. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 4
Abramsky S, Tzevelekos N (2010). Introduction to Categories and Categorical Logic. nameOfConference

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

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/2867

Citations: 0
Tzevelekos N (2010). Program Equivalence with Names.. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 0
Tzevelekos N (2009). FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES. nameOfConference

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

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/3283

Citations: 0
Murawski AS, Tzevelekos N (2009). Full Abstraction for Reduced ML. nameOfConference

DOI: doi

QMRO: qmroHref

Citations: 4
Ong CHL, Tzevelekos N (2009). Functional Reachability. nameOfConference

DOI: 10.1109/LICS.2009.48

QMRO: qmroHref

Citations: 2
Tzevelekos N (2007). Full abstraction for nominal general references. nameOfConference

DOI: 10.1109/LICS.2007.21

QMRO: qmroHref

Citations: 1
Tzevelekos N (2006). Investigations on the dual calculus. nameOfConference

DOI: 10.1016/j.tcs.2006.04.009

QMRO: qmroHref

Citations: 0
Murawski AS, TZEVELEKOS NP (publicationYear). Block Structure vs Scope Extrusion: Between Innocence and Omniscience. nameOfConference

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

QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/13737

Citations: 0

Areas of study

Experience Queen Mary

Study at Queen Mary

Senior Lecturer