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:

Publications

• TZEVELEKOS NP, Murawski AS (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
• Birkedal L, Dinsdale-Young T, Jaber G et al. (2017). Trace Properties from Separation Logic Specifications.. nameOfConference

  
  

  DOI: doi

  
  

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

  
  

  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: 3
• 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