Dr Nikos TzevelekosSenior LecturerEmail: nikos.tzevelekos@qmul.ac.ukTelephone: +44 20 7882 6974Room Number: Peter Landin, CS 434Website: http://www.tzevelekos.orgProfileTeachingResearchPublicationsProfileI am a Senior Lecturer in Computer Science. My research is on theoretical computer science. I study the mathematical meaning of computation. I devise mathematical models of programs and computational processes, and examine applications of these models to program analysis and verification.TeachingAlgorithms 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.ResearchResearch 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.Themes:- Program analysis- Game semantics- Denotational semantics- Automata over infinite alphabetsPublications Koutavas V, Lin Y-Y, Tzevelekos N (2024). An Operational Semantics for Yul.. nameOfConference DOI: doi QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/99499 Koutavas V, Lin Y-Y, Tzevelekos N (2024). Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence.. nameOfConference DOI: doi QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/97148 Bandukara MH, Tzevelekos N (2023). On-the-fly bisimulation equivalence checking for fresh-register automata. nameOfConference DOI: 10.1016/j.sysarc.2023.103010 QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/91423 Tzevelekos N, Murawski AS (2023). Deconstructing general references via game semantics. nameOfConference DOI: 10.1007/978-3-031-24117-8_8 QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/79858 Koutavas V, Lin Y-Y, Tzevelekos N (2023). Fully Abstract Normal Form Bisimulation for Call-by-Value PCF. 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) DOI: 10.1109/lics56636.2023.10175778 QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/91424 Bandukara MH, Tzevelekos N (2022). On-The-Fly Bisimilarity Checking for Fresh-Register Automata. nameOfConference DOI: 10.1007/978-3-031-21213-0_12 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/82367 (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 QMRO: qmroHref Koutavas V, Lin YY, Tzevelekos N (2022). From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques. nameOfConference DOI: 10.1007/978-3-030-99527-0_10 QMRO: https://qmro.qmul.ac.uk/xmlui/handle/123456789/76518 Birkedal L, Dinsdale-Young T, Guéneau A et al. (2021). Theorems for free from separation logic specifications. nameOfConference DOI: 10.1145/3473586 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/73503 Murawski AS, Tzevelekos N (2020). Game Semantics for Interface Middleweight Java.. nameOfConference DOI: 10.1145/3428676 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/67667 Lin YY, Tzevelekos N (2020). Symbolic execution game semantics. nameOfConference DOI: 10.4230/LIPIcs.FSCD.2020.27 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/65063 Murawski AS, Ramsay SJ, Tzevelekos N (2020). Bisimilarity in fresh-register automata.. nameOfConference DOI: doi QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/65062 Lin Y-Y, Tzevelekos N (2020). Symbolic Execution Game Semantics.. nameOfConference DOI: doi QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/65064 Lin Y-Y, Tzevelekos N (2019). A Bounded Model Checking Technique for Higher-Order Programs. nameOfConference DOI: 10.1007/978-3-030-35540-1_1 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/60823 (2019). 12TH PANHELLENIC LOGIC SYMPOSIUM (PLS 12, 2019) CO-SPONSORED BY THE ASSOCIATION FOR SYMBOLIC LOGIC Anogeia, Crete, Greece June 26–30, 2019. nameOfConference DOI: 10.1017/bsl.2019.40 QMRO: qmroHref Murawski AS, Ramsay SJ, Tzevelekos N (2019). DEQ: Equivalence Checker for Deterministic Register Automata. nameOfConference DOI: 10.1007/978-3-030-31784-3_20 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/59154 (publicationYear). title. nameOfConference DOI: 10.4204/eptcs.296 QMRO: qmroHref De Angelis E, Fedyukovich G, Tzevelekos N et al. (2019). Preface. nameOfConference DOI: doi QMRO: qmroHref De Angelis E, Fedyukovich G, Tzevelekos N et al. (publicationYear). Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning. nameOfConference DOI: 10.4204/eptcs.296.0 QMRO: qmroHref TZEVELEKOS NP, Murawski AS (2019). Higher-Order Linearisability. nameOfConference DOI: 10.1016/j.jlamp.2019.01.002 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/55025 Murawski AS, Tzevelekos N (2019). Higher-order linearisability.. nameOfConference DOI: 10.1016/j.jlamp.2019.01.002 QMRO: qmroHref (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.. nameOfConference DOI: doi QMRO: qmroHref Murawski AS, Ramsay SJ, Tzevelekos N (2018). Polynomial-time equivalence testing for deterministic fresh-register automata. nameOfConference DOI: 10.4230/LIPIcs.MFCS.2018.72 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/44616 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://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/36555 Lin Y-Y, Tzevelekos N (2018). Higher-Order Bounded Model Checking. nameOfConference DOI: doi QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/42063 TZEVELEKOS NP, Murawski AS (2017). Algorithmic games for full ground references. nameOfConference DOI: 10.1007/s10703-017-0292-9 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/25859 Murawski AS, Tzevelekos N (2017). Higher-order linearisability. nameOfConference DOI: 10.4230/LIPIcs.CONCUR.2017.34 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/25012 Murawski AS, Tzevelekos N (publicationYear). Block structure vs scope extrusion: between innocence and omniscience. nameOfConference DOI: 10.2168/lmcs-12(3:3)2016 QMRO: qmroHref TZEVELEKOS NP, Murawski AS, Ramsay SJ (2017). Reachability in Pushdown Register Automata. nameOfConference DOI: 10.1016/j.jcss.2017.02.008 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/21819 Birkedal L, Dinsdale-Young T, Jaber G et al. (2017). Trace Properties from Separation Logic Specifications. nameOfConference DOI: doi QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/19600 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://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/25576 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://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/13737 Jaber G, TZEVELEKOS NP (2016). Trace Semantics for Polymorphic References. Logic in Computer Science (LICS) DOI: 10.1145/2933575.2934509 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/13081 Murawski AS, Tzevelekos N (2016). An invitation to game semantics. nameOfConference DOI: 10.1145/2948896.2948902 QMRO: qmroHref Murawski AS, Tzevelekos N (2016). Nominal Game Semantics. nameOfConference DOI: 10.1561/9781680831078 QMRO: qmroHref 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 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 Murawski AS, Ramsay SJ, Tzevelekos N (publicationYear). Bisimilarity in Fresh-Register Automata. 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science DOI: 10.1109/lics.2015.24 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/13504 Igarashi A, Murawski AS, Tzevelekos N (2015). Semantics and Verification of Object-Oriented Languages (NII Shonan Meeting 2015-13).. nameOfConference DOI: doi QMRO: qmroHref Murawski AS, Tzevelekos N (2014). Game semantics for interface middleweight Java. nameOfConference DOI: 10.1145/2578855.2535880 QMRO: qmroHref Murawski AS, Tzevelekos N (2014). Game Semantics for Nominal Exceptions. nameOfConference DOI: 10.1007/978-3-642-54830-7_11 QMRO: qmroHref (2014). Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14. nameOfConference DOI: 10.1145/2535838 QMRO: qmroHref Murawski AS, Ramsay SJ, Tzevelekos N (2014). Reachability in Pushdown Register Automata. nameOfConference DOI: 10.1007/978-3-662-44522-8_39 QMRO: qmroHref Murawski AS, Tzevelekos N (2013). Deconstructing General References via Game Semantics.. nameOfConference DOI: 10.1007/978-3-642-37075-5_16 QMRO: qmroHref Murawski AS, Tzevelekos N (2013). Full abstraction for Reduced ML.. nameOfConference DOI: 10.1016/j.apal.2013.05.007 QMRO: qmroHref Tzevelekos N, Grigore R (2013). History-Register Automata. nameOfConference DOI: 10.1007/978-3-642-37075-5_2 QMRO: qmroHref Tzevelekos N, Grigore R (2013). History-Register Automata.. nameOfConference DOI: 10.2168/LMCS-12(1:7)2016 QMRO: qmroHref Murawski AS, Tzevelekos N (2013). Towards Nominal Abramsky.. nameOfConference DOI: 10.1007/978-3-642-38164-5_17 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/5321 Grigore R, Distefano D, Petersen RL et al. (2012). Runtime Verification Based on Register Automata. nameOfConference DOI: 10.1007/978-3-642-36742-7_19 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/19031 Grigore R, Tzevelekos N (2012). History-Register Automata. nameOfConference DOI: 10.2168/LMCS-12(1:7)2016 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/12585 Ghica DR, Tzevelekos N (2012). A System-Level Semantics. nameOfConference DOI: 10.1016/j.entcs.2012.08.013 QMRO: qmroHref Ghica DR, Tzevelekos N (2012). A System-Level Game Semantics.. nameOfConference DOI: 10.1016/j.entcs.2012.08.013 QMRO: qmroHref Murawski AS, Tzevelekos N (2012). Algorithmic Games for Full Ground References.. nameOfConference DOI: 10.1007/978-3-642-31585-5_30 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/25577 Tzevelekos N (2012). Program equivalence in a simple language with state.. nameOfConference DOI: 10.1016/j.cl.2012.02.002 QMRO: qmroHref Distefano D, Grigore R, Petersen RL et al. (2012). Runtime Verification Based on Register Automata. nameOfConference DOI: doi QMRO: qmroHref Abramsky S, Tzevelekos N (2011). Introduction to Categories and Categorical Logic. nameOfConference DOI: 10.1007/978-3-642-12821-9_1 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/2867 Murawski AS, Tzevelekos N (2011). Algorithmic Nominal Game Semantics.. nameOfConference DOI: 10.1007/978-3-642-19718-5_22 QMRO: qmroHref Tzevelekos N (2011). Fresh-Register Automata. nameOfConference DOI: 10.1145/1926385.1926420 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/7651 Murawski AS, Tzevelekos N (2011). Game semantics for good general references. nameOfConference DOI: 10.1109/LICS.2011.31 QMRO: qmroHref Murawski AS, Tzevelekos N (2010). Block Structure vs. Scope Extrusion: Between Innocence and Omniscience. nameOfConference DOI: 10.1007/978-3-642-12032-9_4 QMRO: qmroHref Tzevelekos N (2010). Program equivalence with names. nameOfConference DOI: doi QMRO: qmroHref Tzevelekos N (2009). FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES. nameOfConference DOI: 10.2168/LMCS-5(3:8)2009 QMRO: https://uat2-qmro.qmul.ac.uk/xmlui/handle/123456789/3283 Murawski AS, Tzevelekos N (2009). Full Abstraction for Reduced ML. nameOfConference DOI: 10.1007/978-3-642-00596-1_4 QMRO: qmroHref 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 Tzevelekos N (2006). Investigations on the dual calculus. nameOfConference DOI: 10.1016/j.tcs.2006.04.009 QMRO: qmroHref