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

 vkoutav@tcd.ie

 3531896 1115


Vasileios Koutavas (PhD and MSc, Northeastern; BSc, NTU Athens) is an Assistant Professor in Software Systems at the School of Computer Science and Statistics. His research is in Theoretical Computer Science, with contributions to programming languages, formal (mathematics-based) methods, and software engineering, translating theory into software-verification techniques and tools. He leads a research programme on the mathematical foundations of software and their application to tools for finding faults and verifying software correctness. His work brings together students, postdoctoral researchers and international collaborators to create techniques and tools that help ensure increasingly AI-generated software is safe to run. He has secured competitive funding from the Irish Research Centre for Software (Lero), the Irish Research Council, Cisco, and the Ethereum Foundation, for developing verification techniques for concurrent software and smart contracts. His research team is a world leader in verifying the safety of code modifications in programs that pass code around as data. Their work has resolved a question open since the 1970s about the mathematical foundations of functional programming. His research advances reversible computing and the verification of software that adapts while interacting with the physical world. He co-invented Reverse Hoare Logic, a precursor to methods now influential in industrial bug finding. His work has earned international recognition, including Distinguished Paper Awards at the leading conferences ACM/IEEE LICS 2023 (ICORE-A*) and SEAMS@ICSE 2018 (ICORE-A), and invited publication in the Journal of the ACM, the flagship journal of the world's pre-eminent computing society.
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