Bisimulations for Untyped Imperative Objects. - Vasileios Koutavas; Mitchell Wand (ESOP, 2006)

Small bisimulations for reasoning about higher-order imperative programs. - Vasileios Koutavas; Mitchell Wand (POPL, 2006)

Liveness of Communicating Transactions (Extended Abstract). - Edsko de Vries; Vasileios Koutavas; Matthew Hennessy (APLAS, 2010)

Communicating Transactions - (Extended Abstract). - Edsko de Vries; Vasileios Koutavas; Matthew Hennessy (CONCUR, 2010)

Limitations of Applicative Bisimulation (Preliminary Report). - Vasileios Koutavas; Paul Blain Levy; Eijiro Sumii (Modelling, Controlling and Reasoning About State, 2010)

A Testing Theory for a Higher-Order Cryptographic Language - (Extended Abstract). - Vasileios Koutavas; Matthew Hennessy (ESOP, 2011)

Reverse Hoare Logic. - Edsko de Vries; Vasileios Koutavas (SEFM, 2011)

From Applicative to Environmental Bisimulation. - Vasileios Koutavas; Paul Blain Levy; Eijiro Sumii (MFPS, 2011)

First-order reasoning for higher-order concurrency. - Vasileios Koutavas; Matthew Hennessy (Comput. Lang. Syst. Struct., 2012)

Symbolic Bisimulation for a Higher-Order Distributed Language with Passivation - (Extended Abstract). - Vasileios Koutavas; Matthew Hennessy (CONCUR, 2013)

Towards Efficient Abstractions for Concurrent Consensus. - Carlo Spaccasassi; Vasileios Koutavas (Trends in Functional Programming, 2013)

Bisimulations for Communicating Transactions - (Extended Abstract). - Vasileios Koutavas; Carlo Spaccasassi; Matthew Hennessy (FoSSaCS, 2014)

Complete session types inference with progress guarantees for ML. - Carlo Spaccasassi; Vasileios Koutavas (CoRR, 2015)

Type-Based Analysis for Session Inference (Extended Abstract). - Carlo Spaccasassi; Vasileios Koutavas (FORTE, 2016)

A Safety and Liveness Theory for Total Reversibility (Extended Abstract). - Claudio Antares Mezzina; Vasileios Koutavas (CoRR, 2016)

A safety and liveness theory for total reversibility. - Claudio Antares Mezzina; Vasileios Koutavas (TASE, 2017)

Locally Nameless Permutation Types. - Edsko de Vries; Vasileios Koutavas (CoRR, 2017)

Self-adaptive automata. - Aimee Borda; Vasileios Koutavas (FormaliSE@ICSE, 2018)

Compositional verification of self-adaptive cyber-physical systems. - Aimee Borda; Liliana Pasquale; Vasileios Koutavas; Bashar Nuseibeh (SEAMS@ICSE, 2018)

Distinguishing between communicating transactions. - Vasileios Koutavas; Maciej Gazda; Matthew Hennessy (Inf. Comput., 2018)

Translation of CCS into CSP, Correct up to Strong Bisimulation. - Gerard Ekembe Ngondi; Vasileios Koutavas; Andrew Butterfield (SEFM, 2021)

There and Back Again: From Bounded Checking to Verification of Program Equivalence via Symbolic Up-to Techniques. - Vasileios Koutavas; Yu-Yang Lin; Nikos Tzevelekos (CoRR, 2021)

From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques. - Vasileios Koutavas; Yu-Yang Lin; Nikos Tzevelekos (TACAS (2), 2022)

From CCS to CSP: the m-among-n Synchronisation Approach. - Gerard Ekembe Ngondi; Vasileios Koutavas; Andrew Butterfield (EXPRESS/SOS, 2022)

Fully Abstract Normal Form Bisimulation for Call-by-Value PCF. - Vasileios Koutavas; Yu-Yang Lin; Nikos Tzevelekos (LICS, 2023)

Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence. - Vasileios Koutavas; Yu-Yang Lin; Nikos Tzevelekos (LICS, 2024)

An Operational Semantics for Yul. - Vasileios Koutavas; Yu-Yang Lin; Nikos Tzevelekos (SEFM, 2024)

Llm-Based Generation of Weakest Preconditions and Precise Array Invariants. - Daragh King; Vasileios Koutavas; Laura Kovács (FormaliSE, 2025)

FuzzFeed: An Automatic Approach to Weakest Precondition Generation using LLMs and Fuzzing. - Daragh King; Vasileios Koutavas; Laura Kovács (CoRR, 2025)