Dr Nikos Tzevelekos

Senior Lecturer
Email: nikos.tzevelekos@qmul.ac.ukTelephone: +44 20 7882 6974Room Number: Peter Landin, CS 434Website: http://www.tzevelekos.org
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.
Logic in Computer Science (Postgraduate)
The module introduces students to Mathematical Logic concepts and their use in Computer Science. The topics covered include: - Propositional Logic and Introduction to Critical Thinking - Solving SAT instances. DPLL algorithm, validity, satisfiability, SAT solvers - Temporal Logics. For example: Linear Temporal Logic, Computation Tree Logic, model checkers (e.g. SPIN) - Predicate Logic. First-order logic, syntax and semantics, satisfiability, SMT solvers - Program Logics. For example, Hoare logic. The module will include exercises and hands-on practicals e.g. using SAT solvers and model checkers.
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
-
Murawski AS, Ramsay SJ, Tzevelekos N (2020). Bisimilarity in fresh-register automata.. nameOfConference
DOI: doi
-
TZEVELEKOS NP, Murawski AS (2019). Higher-Order Linearisability. nameOfConference
-
Lin YY, Tzevelekos N (2019). A bounded model checking technique for higher-order programs. nameOfConference
-
Murawski AS, Ramsay SJ, Tzevelekos N (2019). DEQ: Equivalence Checker for Deterministic Register Automata.. nameOfConference
DOI: doi
-
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)
-
Murawski AS, Ramsay SJ, Tzevelekos N (2018). Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata.. nameOfConference
DOI: doi
-
TZEVELEKOS NP, Murawski AS (2017). Algorithmic games for full ground references. nameOfConference
-
TZEVELEKOS NP, Murawski AS, Ramsay SJ (2017). Reachability in Pushdown Register Automata. nameOfConference
-
Hyland M, McCusker G, Tzevelekos N (2017). Foreword for special issue of APAL for GaLoP 2013. nameOfConference
-
Birkedal L, Dinsdale-Young T, Jaber G et al. (2017). Trace Properties from Separation Logic Specifications.. nameOfConference
DOI: doi
-
Jaber G, TZEVELEKOS NP (2016). Trace Semantics for Polymorphic References. Logic in Computer Science (LICS)
-
TZEVELEKOS NP, Grigore R (2016). History-Register Automata. nameOfConference
-
Murawski AS, Tzevelekos N (2016). BLOCK STRUCTURE VS SCOPE EXTRUSION: BETWEEN INNOCENCE AND OMNISCIENCE. nameOfConference
QMRO: qmroHref -
Murawski AS, Ramsay SJ, Tzevelekos N (2015). A Contextual Equivalence Checker for IMJ. nameOfConference
QMRO: qmroHref -
Murawski AS, Ramsay SJ, Tzevelekos N et al. (2015). Bisimilarity in Fresh-Register Automata. nameOfConference
DOI: 10.1109/LICS.2015.24
-
Murawski AS, Ramsay SJ, Tzevelekos N (2015). Game Semantic Analysis of Equivalence in IMJ. nameOfConference
QMRO: qmroHref -
Murawski AS, Tzevelekos N (2014). Game Semantics for Interface Middleweight Java. nameOfConference
DOI: 10.1145/2535838
QMRO: qmroHref -
Murawski AS, Tzevelekos N (2014). Game semantics for interface middleweight Java.. nameOfConference
DOI: doi
-
Grigore R, Distefano D, Petersen RL et al. (2013). Runtime Verification Based on Register Automata. nameOfConference
DOI: doi
-
Murawski AS, Tzevelekos N (2012). Algorithmic Games for Full Ground References.. nameOfConference
DOI: doi
-
Tzevelekos N (2012). Program equivalence in a simple language with state.. nameOfConference
QMRO: qmroHref -
Tzevelekos N (2011). Fresh-Register Automata. nameOfConference
-
Murawski AS, Tzevelekos N, IEEE (2011). Game semantics for good general references. nameOfConference
DOI: 10.1109/LICS.2011.31
QMRO: qmroHref -
Abramsky S, Tzevelekos N (2010). Introduction to Categories and Categorical Logic. nameOfConference
-
Tzevelekos N (2009). FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES. nameOfConference
-
Ong CHL, Tzevelekos N (2009). Functional Reachability. nameOfConference
DOI: 10.1109/LICS.2009.48
QMRO: qmroHref -
Tzevelekos N (2007). Full abstraction for nominal general references. nameOfConference
DOI: 10.1109/LICS.2007.21
QMRO: qmroHref