| 2022 | PLDI | CycleQ: an efficient basis for cyclic equational reasoning. | Eddie Jones, C.-H. Luke Ong, Steven J. Ramsay |
| 2021 | LICS | Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses. | Toby Cathcart Burn, Luke Ong, Steven J. Ramsay, Dominik Wagner |
| 2019 | ATVA | DEQ: Equivalence Checker for Deterministic Register Automata. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2018 | MFCS | Polynomial-Time Equivalence Testing for Deterministic Fresh-Register Automata. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2015 | ATVA | A Contextual Equivalence Checker for IMJ ∗. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2015 | ATVA | Game Semantic Analysis of Equivalence in IMJ. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2015 | LICS | Bisimilarity in Fresh-Register Automata. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2014 | MFCS | Reachability in Pushdown Register Automata. | Andrzej S. Murawski, Steven J. Ramsay, Nikos Tzevelekos |
| 2014 | POPL | A type-directed abstraction refinement approach to higher-order model checking. | Steven J. Ramsay, Robin P. Neatherway, C.-H. Luke Ong |
| 2014 | PPDP | Exact Intersection Type Abstractions for Safety Checking of Recursion Schemes. | Steven J. Ramsay |
| 2012 | ICFP | A traversal-based algorithm for higher-order model checking. | Robin P. Neatherway, Steven J. Ramsay, C.-H. Luke Ong |
| 2011 | POPL | Verifying higher-order functional programs with pattern-matching algebraic data types. | C.-H. Luke Ong, Steven J. Ramsay |