Skip to main content

Trinity College Dublin, The University of Dublin

Menu Search


Trinity College Dublin By using this website you consent to the use of cookies in accordance with the Trinity cookie policy. For more information on cookies see our cookie policy.

      
Profile Photo

Dr. Vasileios Koutavas

Assistant Professor Software Systems (Computer Science)
OREILLY INSTITUTE
      
Profile Photo

Dr. Vasileios Koutavas

Assistant Professor Software Systems (Computer Science)
OREILLY INSTITUTE


I am an Assistant Professor in Software Systems in the School of Computer Science and Statistics at Trinity College Dublin, a post I have held since 2014. My research builds on the mathematical foundations of programming languages to develop methods and tools for checking that complex software behaves as intended. It spans longstanding work on programming language semantics and concurrency and more recent work on automated software verification and fault detection. At Trinity, I have led a programme of research supported through Lero, the Research Ireland Centre for Software, and by national and industry funders including the Irish Research Council, Cisco and the Ethereum Foundation. I completed my PhD in Computer Science at Northeastern University in 2008 and joined Trinity as a Research Fellow later that year. I served as Associate Director of Undergraduate Teaching and Learning from 2018 to 2026 and have been a College Tutor since 2015. I teach across undergraduate and integrated master's programmes, principally in algorithms, programming and formal verification.
Details Date
Conference PC Member: Technical Papers track, European Conference on Object-Oriented Programming (ECOOP 2027) 2027
Workshop PC Member: Workshop on Program Equivalence and Relational Reasoning (PERR) 2026
Workshop PC Member: Combined International Workshop on Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS) 2026, 2023, 2022, 2018
Conference PC Member: International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE) 2025, 2024
Conference PC Member: International Conference on Mathematical Foundations of Programming Semantics (MFPS) 2023
Conference PC Member: 12th Panhellenic Logic Symposium (PLS12) 2019
Conference PC Member: Service-Oriented Architectures and Programming (SOAP) track, ACM/SIGAPP Symposium on Applied Computing (SAC) 2018, 2017, 2016
Workshop PC Member: Interaction and Concurrency Experience (ICE) 2014
Details Date From Date To
Lero - the Research Ireland Centre for Software - Member from 2008 to Present - Funded Investigator from 2014 to 2026 2008 2026
Daragh King, Vasileios Koutavas, Laura Kovács, LLMs and fuzzing in tandem: a new approach to automatically generating weakest preconditions, International Journal on Software Tools for Technology Transfer, 28, (3), 2026, p317-328 , Journal Article, PUBLISHED  DOI
Daragh King, Vasileios Koutavas, Laura Kovács, LLM-Based Generation of Weakest Preconditions and Precise Array Invariants, 2025 IEEE/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE), Ottawa, ON, Canada, 27-28 April 2025, IEEE, 2025, pp96-100 , Conference Paper, PUBLISHED  DOI
Koutavas V., Lin Y.-Y., Tzevelekos N., Fully Abstract Normal Form Bisimulation for Call-by-Value PCF, Journal of the ACM, 72, (6), 2025, p43:1-43:52 , Journal Article, PUBLISHED  DOI
Vasileios Koutavas, Yu Yang Lin, Nikos Tzevelekos, Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence, LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Tallinn, Estonia, 8-12 July 2024, Association for Computing Machinery, 2024, pp1 - 15, Conference Paper, PUBLISHED  DOI  URL
Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos, An Operational Semantics for Yul, Lecture Notes in Computer Science, Software Engineering and Formal Methods. SEFM 2024, Aveiro, Portugal, 4-8 November 2024, edited by Madeira, Alexandre and Knapp, Alexander , 15280, Springer Nature Switzerland, 2024, pp328 - 346, Conference Paper, PUBLISHED  TARA - Full Text  DOI
Yu-Yang Lin, Vasileios Koutavas, Nikos Tzevelekos, 'YulTracer: Alpha 0.1.1', An Operational Semantics for Yul, 0.1.1, Zenodo, 2024, -, Notes: [YulTracer 0.1.1 is an OCaml implementation of the small-step operational semantics presented in "An Operational Semantics for Yul," SEFM 2024, DOI: 10.1007/978-3-031-77382-2_19. The artefact received the SEFM 2024 Artifacts Evaluated-Reusable and Artifacts Available badges.], Software, PUBLISHED  DOI  URL
Vasileios Koutavas; Yu-Yang Lin; Nikos Tzevelekos, Fully Abstract Normal Form Bisimulation for Call-by-Value PCF, 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Boston, MA, USA, 26-29 June 2023, IEEE, 2023, pp1 - 13, Conference Paper, PUBLISHED  TARA - Full Text  DOI
Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos, From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques, LNCS, 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (ETAPS 2022), Munich, Germany, 2-7 April 2022, 13244, Springer, 2022, pp178 - 195, Conference Paper, PUBLISHED  TARA - Full Text  DOI  URL
Gerard Ekembe Ngondi, Vasileios Koutavas, Andrew Butterfield, From CCS to CSP: the m-among-n Synchronisation Approach, Electronic Proceedings in Theoretical Computer Science, Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics, Warsaw, Poland, 12th September 2022, edited by Valentina Castiglioni, Claudio Antares. , Open Publishing Association, 2022, pp60 - 74, Conference Paper, PUBLISHED  TARA - Full Text  DOI
Gerard Ekembe Ngondi, Vasileios Koutavas, Andrew Butterfield, Translation of CCS into CSP, Correct up to Strong Bisimulation, Springer LNCS, Software Engineering and Formal Methods (SEFM 21), online, 6-10th December 2021, edited by Radu Calinescu, Corina S. Pasareanu , 13085, Springer, 2021, pp243 - 261, Conference Paper, PUBLISHED  TARA - Full Text  DOI
  

Page 1 of 3
Yu-Yang Lin, Vasileios Koutavas, Nikos Tzevelekos, 'Hobbit-PDNF: Pushdown Normal-Form Bisimulation Tool', Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence, v1.0.0, Zenodo, 2024, -, Notes: [This archived elease accompanied "Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence," LICS 2024, DOI: 10.1145/3661814.3662103.], Software, PUBLISHED
Yu-Yang Lin, Vasileios Koutavas, Nikos Tzevelekos, 'pcfeq: Bisimulation Checking Tool for Call-by-Value PCF Programs', Fully Abstract Normal Form Bisimulation for Call-by-Value PCF, Zenodo, 2023, -, Notes: [Implements the methods presented in "Fully Abstract Normal Form Bisimulation for Call-by-Value PCF," LICS 2023, DOI: 10.1109/LICS56636.2023.10175778, and subsequently extended in Journal of the ACM 72(6), article 43, 2025, DOI: 10.1145/3765737. The software accompanied the publications.], Software, PUBLISHED
Yu-Yang Lin, Vasileios Koutavas, Nikos Tzevelekos, 'Hobbit: Higher Order Bounded Bisimulation Tool', From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques., Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, 2022, -, Notes: [Open-source software accompanying "From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques," TACAS 2022, paper DOI: 10.1007/978-3-030-99527-0_10.], Software, PUBLISHED
Vasileios Koutavas, Maciej Gazda, Matthew Hennessy, Distinguishing between Communicating Transactions, CoRR abs/1703.03256, 2017, Report, PUBLISHED
Edsko de Vries, Vasileios Koutavas, Locally Nameless Permutation Types, CoRR, abs/1710.08444, Arxiv - The Computing Research Repository (CoRR), 2017, Report, PUBLISHED
Claudio Antares Mezzina, Vasileios Koutavas, A Safety and Liveness Theory for Total Reversibility (Extended Abstract), CoRR abs/1604.05555, Arxiv - The Computing Research Repository (CoRR), 2016, Report, PUBLISHED
Carlo Spaccasassi, Vasileios Koutavas, Complete session types inference with progress guarantees for ML, CoRR abs/1510.03929, Arxiv - The Computing Research Repository (CoRR), 2015, Report, PUBLISHED
Carlo Spaccasassi, Vasileios Koutavas, Towards Efficient Abstractions for Concurrent Consensus, CoRR abs/1304.1913, Arxiv - The Computing Research Repository (CoRR), 2013, Report, PUBLISHED
Vasileios Koutavas, Paul Blain Levy, Eijiro Sumii, Limitations of Applicative Bisimulation (Preliminary Report), 10351, 1862-4405, Dagstuhl Seminar Proceedings, Modelling, Controlling and Reasoning About State, Dagstuhl, 2010, Report, PUBLISHED

  


Award Date
Distinguished Paper Award, LICS 2023, for "Fully Abstract Normal Form Bisimulation for Call-by-Value PCF"; the paper was one of two distinguished papers invited to submit an extended version to the Journal of the ACM, where it was published in 2025. 26 June 2023
Distinguished Paper Award, SEAMS 2018, for "Compositional Verification of Self-Adaptive Cyber-Physical Systems". 28 May 2018