Skip to main content
Research

Publications: Dr Nikolaos Tzevelekos

Koutavas V, Lin Y-Y, Tzevelekos N ( 2022 ) . From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques . vol. 13244 , 178 - 195 .
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 ,
Koutavas V, Lin Y-Y, Tzevelekos N ( 2021 ) . From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques .
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 .
Lin Y-Y, Tzevelekos N ( 2020 ) . Symbolic Execution Game Semantics .
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 .
Eleftheriou P, Tzevelekos N, Pheidas T ( 2019 ) . 12TH PANHELLENIC LOGIC SYMPOSIUM (PLS 12, 2019): CO-SPONSORED by the ASSOCIATION for SYMBOLIC LOGIC . Bulletin of Symbolic Logic vol. 25 , ( 3 )
( 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 ,
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 .
TZEVELEKOS NP, Murawski AS ( 2019 ) . Higher-Order Linearisability . Journal of Logical and Algebraic Methods in Programming
Lin YY, Tzevelekos N ( 2019 ) . A bounded model checking technique for higher-order programs . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 11951 LNCS , 1 - 18 .
Murawski AS, Ramsay SJ, Tzevelekos N ( 2019 ) . DEQ: Equivalence Checker for Deterministic Register Automata . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 11781 LNCS , 350 - 356 .
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 ,
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 ) . Higher-Order Linearisability .
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 ) . Block structure vs scope extrusion: between innocence and omniscience .
Jaber G, Tzevelekos N ( 2016 ) . Trace semantics for polymorphic references .
Murawski AS, Tzevelekos N ( 2016 ) . Block structure vs scope extrusion: Between innocence and omniscience . Logical Methods in Computer Science vol. 12 , ( 3 )
Murawski AS, Tzevelekos N ( 2016 ) . Nominal Game Semantics .
Murawski AS, Ramsay SJ, Tzevelekos N ( 2015 ) . Bisimilarity in fresh-register automata . Proceedings - Symposium on Logic in Computer Science . vol. 2015-July , 156 - 167 .
Murawski AS, Ramsay SJ, Tzevelekos N ( 2015 ) . A Contextual Equivalence Checker for IMJ . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 9364 , 234 - 240 .
Murawski AS, Ramsay SJ, Tzevelekos N ( 2015 ) . Game semantic analysis of equivalence in IMJ . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 9364 , 411 - 428 .
Murawski AS, Tzevelekos N ( 2015 ) . Nominal game semantics . Foundations and Trends in Programming Languages vol. 2 , ( 4 ) 191 - 269 .
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 . Conference Record of the Annual ACM Symposium on Principles of Programming Languages . 517 - 528 .
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 interface middleweight java . ACM SIGPLAN Notices . vol. 49 , 517 - 528 .
Murawski AS, Tzevelekos N ( 2014 ) . Game semantics for nominal exceptions . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 8412 LNCS , 164 - 179 .
Murawski AS, Ramsay SJ, Tzevelekos N ( 2014 ) . Reachability in pushdown register automata . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 8634 LNCS , 464 - 473 .
Tzevelekos N, Grigore R ( 2013 ) . History-register automata . vol. 7794 LNCS ,
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 . 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, IEEE ( 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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) . vol. 6014 LNCS , 33 - 47 .
Tzevelekos N ( 2010 ) . Program Equivalence with Names . Modelling, Controlling and Reasoning About State . Editors: Ahmed, A, Benton, N, Birkedal, L, Hofmann, M et al. , vol. 10351 ,
Tzevelekos N ( 2009 ) . Full abstraction for nominal general references .
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 .