Algebras for Program Correctness in Isabelle/HOL. - Alasdair Armstrong; Victor B. F. Gomes; Georg Struth (RAMiCS, 2014)

Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools. - Alasdair Armstrong; Victor B. F. Gomes; Georg Struth (FM, 2014)

Lightweight Program Construction and Verification Tools in Isabelle/HOL. - Alasdair Armstrong; Victor B. F. Gomes; Georg Struth (SEFM, 2014)

Kleene Algebra with Tests and Demonic Refinement Algebras. - Alasdair Armstrong; Victor B. F. Gomes; Georg Struth (Arch. Formal Proofs, 2014)

Principles for Verification Tools: Separation Logic. - Brijesh Dongol; Victor B. F. Gomes; Georg Struth (CoRR, 2014)

A Program Construction and Verification Tool for Separation Logic. - Brijesh Dongol; Victor B. F. Gomes; Georg Struth (MPC, 2015)

Residuated Lattices. - Victor B. F. Gomes; Georg Struth (Arch. Formal Proofs, 2015)

Algebraic principles for program correctness tools in Isabelle/HOL. - Victor Borges Ferreira Gomes (2015)

Modal Kleene Algebra Applied to Program Correctness. - Victor B. F. Gomes; Georg Struth (FM, 2016)

Kleene Algebras with Domain. - Victor B. F. Gomes; Walter Guttmann; Peter Höfner; Georg Struth; Tjark Weber (Arch. Formal Proofs, 2016)

Program Construction and Verification Components Based on Kleene Algebra. - Victor B. F. Gomes; Georg Struth (Arch. Formal Proofs, 2016)

Building program construction and verification tools from algebraic principles. - Alasdair Armstrong; Victor B. F. Gomes; Georg Struth (Formal Aspects Comput., 2016)

Programming and Proving with Classical Types. - Cristina Matache; Victor B. F. Gomes; Dominic P. Mulligan (APLAS, 2017)

Partial Semigroups and Convolution Algebras. - Brijesh Dongol; Victor B. F. Gomes; Ian J. Hayes; Georg Struth (Arch. Formal Proofs, 2017)

A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes. - Victor B. F. Gomes; Martin Kleppmann; Dominic P. Mulligan; Alastair R. Beresford (Arch. Formal Proofs, 2017)

The LambdaMu-calculus. - Cristina Matache; Victor B. F. Gomes; Dominic P. Mulligan (Arch. Formal Proofs, 2017)

Verifying strong eventual consistency in distributed systems. - Victor B. F. Gomes; Martin Kleppmann; Dominic P. Mulligan; Alastair R. Beresford (Proc. ACM Program. Lang., 2017)

OpSets: Sequential Specifications for Replicated Datatypes. - Martin Kleppmann; Victor B. F. Gomes; Dominic P. Mulligan; Alastair R. Beresford (Arch. Formal Proofs, 2018)

OpSets: Sequential Specifications for Replicated Datatypes (Extended Version). - Martin Kleppmann; Victor B. F. Gomes; Dominic P. Mulligan; Alastair R. Beresford (CoRR, 2018)

Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C. - Stella Lau; Victor B. F. Gomes; Kayvan Memarian; Jean Pichon-Pharabod; Peter Sewell (CAV (1), 2019)

Interleaving anomalies in collaborative text editors. - Martin Kleppmann; Victor B. F. Gomes; Dominic P. Mulligan; Alastair R. Beresford (PaPoC@EuroSys, 2019)

Exploring C semantics and pointer provenance. - Kayvan Memarian; Victor B. F. Gomes; Brooks Davis; Stephen Kell; Alexander Richardson 001; Robert N. M. Watson; Peter Sewell (Proc. ACM Program. Lang., 2019)

A Highly-Available Move Operation for Replicated Trees. - Martin Kleppmann; Dominic P. Mulligan; Victor B. F. Gomes; Alastair R. Beresford (IEEE Trans. Parallel Distributed Syst., 2022)