Verifying strong eventual consistency in distributed systems VBF Gomes, M Kleppmann, DP Mulligan, AR Beresford Proceedings of the ACM on Programming Languages 1 (OOPSLA), 1-28, 2017 | 76 | 2017 |
Building program construction and verification tools from algebraic principles A Armstrong, VBF Gomes, G Struth Formal Aspects of Computing 28, 265-293, 2016 | 46 | 2016 |
Exploring C semantics and pointer provenance K Memarian, VBF Gomes, B Davis, S Kell, A Richardson, RNM Watson, ... Proceedings of the ACM on Programming Languages 3 (POPL), 1-32, 2019 | 44 | 2019 |
Kleene algebra A Armstrong, G Struth, T Weber Archive of Formal Proofs 324, 2013 | 41* | 2013 |
A program construction and verification tool for separation logic B Dongol, VBF Gomes, G Struth Mathematics of Program Construction: 12th International Conference, MPC 2015 …, 2015 | 31 | 2015 |
Modal Kleene algebra and partial correctness B Möller, G Struth Algebraic Methodology and Software Technology: 10th International Conference …, 2004 | 30 | 2004 |
Modal Kleene algebra applied to program correctness VBF Gomes, G Struth FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus …, 2016 | 21 | 2016 |
Algebraic principles for rely-guarantee style concurrency verification tools A Armstrong, VBF Gomes, G Struth FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12-16 …, 2014 | 17 | 2014 |
Kleene algebra with tests and demonic refinement algebras A Armstrong, VBF Gomes, G Struth Archive of Formal Proofs 2014, 2014 | 16 | 2014 |
Interleaving anomalies in collaborative text editors M Kleppmann, VBF Gomes, DP Mulligan, AR Beresford Proceedings of the 6th Workshop on Principles and Practice of Consistency …, 2019 | 13 | 2019 |
Cerberus-BMC: A principled reference semantics and exploration tool for concurrent and sequential C S Lau, VBF Gomes, K Memarian, J Pichon-Pharabod, P Sewell Computer Aided Verification: 31st International Conference, CAV 2019, New …, 2019 | 11 | 2019 |
Algebras for program correctness in Isabelle/HOL A Armstrong, VBF Gomes, G Struth Relational and Algebraic Methods in Computer Science: 14th International …, 2014 | 11 | 2014 |
A highly-available move operation for replicated trees and distributed filesystems M Kleppmann, DP Mulligan, VBF Gomes, AR Beresford Work-in-progress draft. University of Cambridge, 33, 2020 | 10* | 2020 |
OpSets: Sequential specifications for replicated datatypes (extended version) M Kleppmann, VBF Gomes, DP Mulligan, AR Beresford arXiv preprint arXiv:1805.04263, 2018 | 10 | 2018 |
A framework for establishing strong eventual consistency for conflict-free replicated datatypes VBF Gomes, M Kleppmann, DP Mulligan, AR Beresford Archive of Formal Proofs 2017, 2017 | 9 | 2017 |
Lightweight program construction and verification tools in Isabelle/HOL A Armstrong, VBF Gomes, G Struth Software Engineering and Formal Methods: 12th International Conference, SEFM …, 2014 | 7 | 2014 |
Partial semigroups and convolution algebras B Dongol, VBF Gomes, IJ Hayes, G Struth Arch. Formal Proofs 2017, 2017 | 5 | 2017 |
GRID-CITY: A framework to share smart grids communication with smart city applications GC Heck, R Hexsel, VB Gomes, L Iantorno, LL Junior, T Santana 2021 IEEE International Smart Cities Conference (ISC2), 1-4, 2021 | 4 | 2021 |
Linguistic and non-linguistic cues to acquiring the strong distributivity of each T Knowlton, V Gomes Proceedings of the Linguistic Society of America 7 (1), 5236, 2022 | 3 | 2022 |
Residuated lattices VBF Gomes, G Struth Archive of Formal Proofs, 2016 | 3 | 2016 |