Publications: Dr Nikolaos Tzevelekos

Koutavas V, Lin Y-Y, Tzevelekos N ( 2024 ) . An Operational Semantics for Yul . Lecture Notes in Computer Science vol. 15280 , 328 - 346 .

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

Koutavas V, Lin Y-Y, Tzevelekos N ( 2024 ) . Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence . LICS . Editors: Sobocinski, P, Lago, UD, Esparza, J , 53:1 - 53:1 .

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

Tzevelekos N, Murawski AS ( 2023 ) . Deconstructing general references via game semantics . Samson Abramsky on Logic and Structure in Computer Science and Beyond

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

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

( 2022 ) . Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science . Conference: LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science

Koutavas V, Lin YY, Tzevelekos N ( 2022 ) . From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 13244 LNCS , 178 - 195 .

Birkedal L, Dinsdale-Young T, Guéneau A, Jaber G, Svendsen K, Tzevelekos N ( 2021 ) . Theorems for free from separation logic specifications . Proceedings of the ACM on Programming Languages . vol. 5 , 1 - 29 .

Murawski AS, Tzevelekos N ( 2020 ) . Game Semantics for Interface Middleweight Java . J. ACM vol. 68 , Article 1 , 4:1 - 4:1 .

Lin YY, Tzevelekos N ( 2020 ) . Symbolic execution game semantics . Leibniz International Proceedings in Informatics, LIPIcs vol. 167 ,

Murawski AS, Ramsay SJ, Tzevelekos N ( 2020 ) . Bisimilarity in fresh-register automata . CoRR vol. abs/2005.06411 ,

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

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

( 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 vol. 25 , ( 3 ) 420 - 420 .

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

( 2019 ) . . vol. 296 ,

De Angelis E, Fedyukovich G, Tzevelekos N, Ulbrich M ( 2019 ) . Preface . Electronic Proceedings in Theoretical Computer Science, EPTCS . vol. 296 ,

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

TZEVELEKOS NP, Murawski AS ( 2019 ) . Higher-Order Linearisability . Journal of Logical and Algebraic Methods in Programming

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

( 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 . Editors: Angelis, ED, Fedyukovich, G, Tzevelekos, N, Ulbrich, M et al. , vol. 296 ,

Murawski AS, Ramsay SJ, Tzevelekos N ( 2018 ) . Polynomial-time equivalence testing for deterministic fresh-register automata . Leibniz International Proceedings in Informatics, LIPIcs . vol. 117 ,

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

Lin Y-Y, Tzevelekos N ( 2018 ) . Higher-Order Bounded Model Checking . arXiv

TZEVELEKOS NP, Murawski AS ( 2017 ) . Algorithmic games for full ground references . Formal Methods in System Design

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

Murawski AS, Tzevelekos N ( 2017 ) . Block structure vs scope extrusion: between innocence and omniscience . Logical Methods in Computer Science vol. Volume 12, Issue 3 ,

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

Birkedal L, Dinsdale-Young T, Jaber G, Svendsen K, Tzevelekos N ( 2017 ) . Trace Properties from Separation Logic Specifications .

Hyland M, McCusker G, Tzevelekos N ( 2017 ) . Foreword for special issue of APAL for GaLoP 2013 . ANNALS OF PURE AND APPLIED LOGIC vol. 168 , ( 2 ) 233 - 233 .

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

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

Murawski AS, Tzevelekos N ( 2016 ) . An invitation to game semantics . ACM SIGLOG News vol. 3 , ( 2 ) 56 - 67 .

Murawski AS, Tzevelekos N ( 2016 ) . Nominal Game Semantics . Now Publishers

Murawski AS, Ramsay SJ, Tzevelekos N ( 2015 ) . A Contextual Equivalence Checker for IMJ* . Lecture Notes in Computer Science . vol. 9364 , 234 - 240 .

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

Murawski AS, Ramsay SJ, Tzevelekos N . Bisimilarity in Fresh-Register Automata . Proceedings 11th Annual IEEE Symposium on Logic in Computer Science . Conference: 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science156 - 167 .

Igarashi A, Murawski AS, Tzevelekos N ( 2015 ) . Semantics and Verification of Object-Oriented Languages (NII Shonan Meeting 2015-13) . NII Shonan Meet. Rep. vol. 2015 ,

Murawski AS, Tzevelekos N ( 2014 ) . Game semantics for interface middleweight Java . ACM SIGPLAN Notices vol. 49 , ( 1 ) 517 - 528 .

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

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

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

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

Murawski AS, Tzevelekos N ( 2013 ) . Full abstraction for Reduced ML . Ann. Pure Appl. Log. vol. 164 , Article 11 , 1118 - 1143 .

Tzevelekos N, Grigore R ( 2013 ) . History-Register Automata . Foundations of Software Science and Computation Structures , vol. 7794 , Springer Nature

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

Murawski AS, Tzevelekos N ( 2013 ) . Towards Nominal Abramsky . Computation, Logic, Games, and Quantum Foundations . Editors: Coecke, B, Ong, L, Panangaden, P , vol. 7860 , 246 - 263 .

Grigore R, Distefano D, Petersen RL, Tzevelekos N ( 2012 ) . Runtime Verification Based on Register Automata .

Grigore R, Tzevelekos N ( 2012 ) . History-Register Automata . March vol. 29 ,

Ghica DR, Tzevelekos N ( 2012 ) . A System-Level Semantics .

Ghica DR, Tzevelekos N ( 2012 ) . A System-Level Game Semantics . MFPS vol. 286 , 191 - 211 .

Murawski AS, Tzevelekos N ( 2012 ) . Algorithmic Games for Full Ground References . ICALP (2) vol. 7392 , 312 - 324 .

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

Distefano D, Grigore R, Petersen RL, Tzevelekos N ( 2012 ) . Runtime Verification Based on Register Automata . CoRR vol. abs/1209.5325 ,

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

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

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

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

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

Tzevelekos N ( 2010 ) . Program equivalence with names . Dagstuhl Seminar Proceedings . vol. 10351 ,

Tzevelekos N ( 2009 ) . FULL ABSTRACTION FOR NOMINAL GENERAL REFERENCES . LOG METH COMPUT SCI vol. 5 , ( 3 ) Article 8 ,

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

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

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

Tzevelekos N ( 2006 ) . Investigations on the dual calculus . THEOR COMPUT SCI vol. 360 , ( 1-3 ) 289 - 326 .