Victor Gomes

Research Associate
University of Cambridge

victor.gomes@cl.cam.ac.uk
University of Cambridge
Computer Laboratory
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD, UK

---

Publications

My publications are also available on DBLP.

Journal papers

• Building Program Construction and Verification Tools from Algebraic Principles
  A. Armstrong, V. B. F. Gomes and G. Struth. Formal Aspects of Computing (2016).
  [doi] [abstract] [bibtex] [Isabelle/HOL files]

  Abstract. We present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with tests for the control flow of while-programs and their standard relational semantics for the data flow. It is expanded to a basic program construction tool by adding an operation for the specification statement and one single axiom. To include recursive procedures, Kleene algebras with tests are expanded further to quantales with tests. In this more expressive setting, iteration and the specification statement can be defined explicitly and stronger program transformation rules can be derived. Programming our approach in the Isabelle/HOL interactive theorem prover yields simple lightweight mathematical components as well as program construction and verification tools that are correct by construction themselves. Verification condition generation and program construction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. A number of examples shows our tools at work.

  @article{ArmstrongGS15,
    author    = {Alasdair Armstrong and
                 Victor B. F. Gomes and
                 Georg Struth},
    title     = {Building Program Construction and Verification Tools from
      Algebraic Principles},
    journal   = {Formal Aspects of Computing},
    pages     = {1-29},
    publisher = {Springer London},
    year      = {2015}
  }
  




Conference papers

• Modal Kleene Algebra Applied to Program Correctness
  V. B. F. Gomes and G. Struth. FM'16.
  [pdf] [abstract] [bibtex] [Isabelle/HOL files]

  Abstract. Modal Kleene algebras are relatives of dynamic logics that support program construction and verification by equational reasoning. We describe their application in implementing versatile program correctness components in interactive theorem provers such as Isabelle/HOL. Starting from a weakest precondition based component with a simple relational store model, we show how variants for Hoare logic, strongest postconditions and program refinement can be built in a principled way. Modularity of the approach is demonstrated by variants that capture program termination and recursion, memory models for programs with pointers, and program trace semantics.

  @inproceedings{GomesS16,
    author    = {Victor B. F. Gomes and
                 Georg Struth},
    title     = {Modal Kleene Algebra Applied to Program Correctness},
    booktitle = {{FM}},
    series    = {Lecture Notes in Computer Science},
    volume    = {9995},
    pages     = {310--325},
    year      = {2016}
  }
  



• A Program Construction and Verification Tool for Separation Logic
  B. Dongol, V. B. F. Gomes and G. Struth. MPC'15.
  [pdf] [abstract] [bibtex] [Isabelle/HOL files]

  Abstract. An algebraic approach to the design of program construction and verification tools is applied to separation logic. The control-flow level is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data domain is captured by concrete store-heap models. These are linked to the separation algebra by soundness proofs. Verification conditions and transformation or refinement laws are derived by equational reasoning within the predicate transformer quantale. This separation of concerns makes an implementation in the Isabelle/HOL proof assistant simple and highly automatic. The resulting tool is itself correct by construction; it is explained on three simple examples.

  @inproceedings{DongolGS15,
    author    = {Brijesh Dongol and
                 Victor B. F. Gomes and
                 Georg Struth},
    editor    = {Ralf Hinze and
                 Janis Voigtl{\"{a}}nder},
    title     = {A Program Construction and Verification Tool for Separation Logic},
    booktitle = {{MPC} 2015},
    series    = {Lecture Notes in Computer Science},
    volume    = {9129},
    pages     = {137--158},
    publisher = {Springer},
    year      = {2015}
  }
  



• Lightweight Program Construction and Verification Tools in Isabelle/HOL
  A. Armstrong, V. B. F. Gomes and G. Struth. SEFM'14. (Best Paper Award)
  [pdf] [abstract] [bibtex] [Isabelle/HOL files] [slides]

  Abstract. We present a principled approach to the development of construction and verification tools for while-programs. Our verification tool uses Kleene algebra with tests to capture the control flow of programs and its relational semantics for their data flow. It is extended to a Morgan-style program construction tool by adding one single axiom to the algebra. Our formalisation in Isabelle/HOL makes these tools themselves correct by construction. Verification condition generation and program construction steps are based on simple equational reasoning and supported by powerful Isabelle tactics. Two case studies on program construction and verification show our tools at work.

  @inproceedings{ArmstrongGS14c,
    author    = {Alasdair Armstrong and
                 Victor B. F. Gomes and
                 Georg Struth},
    title     = {Lightweight Program Construction and Verification Tools in
  {I}sabelle/{HOL}},
    booktitle = {{SEFM} 2014},
    pages     = {5--19},
    year      = {2014},
    editor    = {Dimitra Giannakopoulou and
                 Gwen Sala{\"{u}}n},
    series    = {Lecture Notes in Computer Science},
    volume    = {8702},
    publisher = {Springer}
  }
  



• Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools
  A. Armstrong, V. B. F. Gomes and G. Struth. FM'14.
  [pdf] [abstract] [bibtex] [Isabelle/HOL files]

  Abstract. We provide simple equational principles for deriving rely-guarantee-style inference rules and refinement laws based on idempotent semirings. We link the algebraic layer with concrete models of programs based on languages and execution traces. We have implemented the approach in Isabelle/HOL as a lightweight concurrency verification tool that supports reasoning about the control and data flow of concurrent programs with shared variables at different levels of abstraction. This is illustrated on a simple verification example.

  @inproceedings{ArmstrongGS14b,
    author    = {Alasdair Armstrong and
                 Victor B. F. Gomes and
                 Georg Struth},
    title     = {Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools},
    booktitle = {{FM} 2014},
    pages     = {78--93},
    year      = {2014},
    editor    = {Cliff B. Jones and
                 Pekka Pihlajasaari and
                 Jun Sun},
    series    = {Lecture Notes in Computer Science},
    volume    = {8442},
    publisher = {Springer}
  }
  



• Algebras for Program Correctness in Isabelle/HOL
  A. Armstrong, V. B. F. Gomes and G. Struth. RAMiCS'14.
  [pdf] [abstract] [bibtex] [Isabelle/HOL files] [slides]

  Abstract. We present a reference formalisation of Kleene algebra and demonic refinement algebra with tests in Isabelle/HOL. It provides three different formalisations of tests. Our structured comprehensive libraries for these algebras extend an existing Kleene algebra library. It includes an algebraic account of Hoare logic for partial correctness and several refinement and concurrency control laws in a total correctness setting. Formalisation examples include a complex refinement theorem, a generic proof of a loop transformation theorem for partial and total correctness and a simple prototypical verification tool for while programs, which is itself formally verified.

  @inproceedings{ArmstrongGS14a,
    author    = {Alasdair Armstrong and
                 Victor B. F. Gomes and
                 Georg Struth},
    title     = {Algebras for Program Correctness in {I}sabelle/{HOL}},
    booktitle = {{RAMICS} 2014},
    pages     = {49--64},
    year      = {2014},
    editor    = {Peter H{\"{o}}fner and
                 Peter Jipsen and
                 Wolfram Kahl and
                 Martin Eric M{\"{u}}ller},
    series    = {Lecture Notes in Computer Science},
    volume    = {8428},
    publisher = {Springer}
  }
  




Archive of Formal Proofs

• Kleene Algebra with Domain
  V. B. F. Gomes, W. Guttmann, P. Höfner, G. Struth, T. Weber Archive of Formal Proofs (2016).
  [url] [abstract] [bibtex]

  Abstract. Kleene algebras with domain are Kleene algebras endowed with an operation that maps each element of the algebra to its domain of definition (or its complement) in abstract fashion. They form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis.

  @article{GomesGHSW16,
    author    = {Victor B. F. Gomes and
                 Walter Guttmann and
                 Peter H{\"{o}}fner and
                 Georg Struth and
                 Tjark Weber},
    title     = {Kleene Algebras with Domain},
    journal   = {Archive of Formal Proofs},
    volume    = {2016},
    year      = {2016}
  }
  



• Program Construction and Verification Components Based on Kleene Algebra
  V. B. F. Gomes and G. Struth. Archive of Formal Proofs (2016).
  [url] [abstract] [bibtex]

  Abstract. Variants of Kleene algebra support program construction and verification by algebraic reasoning. This entry provides a verification component for Hoare logic based on Kleene algebra with tests, verification components for weakest preconditions and strongest postconditions based on Kleene algebra with domain and a component for step-wise refinement based on refinement Kleene algebra with tests. In addition to these components for the partial correctness of while programs, a verification component for total correctness based on divergence Kleene algebras and one for (partial correctness) of recursive programs based on domain quantales are provided. Finally we have integrated memory models for programs with pointers and a program trace semantics into the weakest precondition component.

  @article{GomesS16,
    author    = {Victor B. F. Gomes and
                 Georg Struth},
    title     = {Program Construction and Verification Components Based on {K}leene Algebra},
    journal   = {Archive of Formal Proofs},
    volume    = {2016},
    year      = {2016}
  }
  



• Residuated Lattices
  V. B. F. Gomes and G. Struth. Archive of Formal Proofs (2015).
  [url] [abstract] [bibtex]

  Abstract. The theory of residuated lattices, first proposed by Ward and Dilworth, is formalised in Isabelle/HOL. This includes concepts of residuated functions; their adjoints and conjugates. It also contains necessary and sufficient conditions for the existence of these operations in an arbitrary lattice. The mathematical components for residuated lattices are linked to the AFP entry for relation algebra. In particular, we prove Jonsson and Tsinakis conditions for a residuated boolean algebra to form a relation algebra.

  @article{GomesGS15,
    author    = {Victor B. F. Gomes and
                 Georg Struth},
    title     = {Residuated Lattices},
    journal   = {Archive of Formal Proofs},
    volume    = {2015},
    year      = {2015}
  }
  



• Kleene Algebra with Tests and Demonic Refinement Algebras
  A. Armstrong, V. B. F. Gomes and G. Struth. Archive of Formal Proofs (2014).
  [url] [abstract] [bibtex]

  Abstract. We formalise Kleene algebra with tests (KAT) and demonic refinement algebra (DRA) in Isabelle/HOL. KAT is relevant for program verification and correctness proofs in the partial correctness setting. While DRA targets similar applications in the context of total correctness. Our formalisation contains the two most important models of these algebras: binary relations in the case of KAT and predicate transformers in the case of DRA. In addition, we derive the inference rules for Hoare logic in KAT and its relational model and present a simple formally verified program verification tool prototype based on the algebraic approach.

  @article{ArmstrongGS14,
    author    = {Alasdair Armstrong and
                 Victor B. F. Gomes and
                 Georg Struth},
    title     = {Kleene Algebra with Tests and Demonic Refinement Algebras},
    journal   = {Archive of Formal Proofs},
    volume    = {2014},
    year      = {2014}
  }
  




PhD Thesis

• Algebraic Principles for Program Correctness Tools in Isabelle/HOL
  V. B. F. Gomes. PhD Thesis, University of Sheffield. 2016.
  [pdf] [abstract] [bibtex] [Isabelle/HOL files]

  Abstract. This thesis puts forward a flexible and principled approach to the development of construction and verification tools for imperative pro- grams, in which the control flow and the data level are cleanly sep- arated. The approach is inspired by algebraic principles and bene- fits from an algebraic semantics layer. It is programmed in the Is- abelle/HOL interactive theorem prover and yields simple lightweight mathematical components as well as program construction and veri- fication tools that are themselves correct by construction. First, a simple tool is implemented using Kleeene algebra with tests (KAT) for the control flow of while-programs, which is the most com- pact verification formalism for imperative programs, and their stan- dard relational semantics for the data level. A reference formalisation of KAT in Isabelle/HOL is then presented, providing three different formalisations of tests. The structured comprehensive libraries for these algebras include an algebraic account of Hoare logic for par- tial correctness. Verification condition generation and program con- struction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving. Second, the tool is expanded to support different programming fea- tures and verification methods. A basic program construction tool is developed by adding an operation for the specification statement and one single axiom. To include recursive procedures, KATs are expanded further to quantales with tests, where iteration and the specification statement can be defined explicitly. Additionally, a nondeterministic extension supports the verification of simple concurrent programs. Finally, the approach is also applied to separation logic, where the control-flow is modelled by power series with convolution as sepa- rating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data level is cap- tured by concrete store-heap models. These are linked to the algebra by soundness proofs. A number of examples shows the tools at work.

  @phdthesis{GomesThesis,
    author       = {Victor B. F. Gomes}, 
    title        = {Algebraic Principles for Program Correctness Tools in {I}sabelle/{HOL}},
    school       = {University of Sheffield},
    year         = 2016,
    month        = 2
  }
  




Master Dissertation

• Controllers for Navigation using Reinforcement Learning
  V. B. F. Gomes. Master dissertation, University of Sheffield and INSA Lyon (2012).
  [pdf] [abstract] [bibtex] [source files]

  Abstract. Understanding the human brain and its behaviour is the main aim of Neuroscience, therefore forming a model with the objective of imitating a special biological behaviour, like the ability to learn, is a research problem with many potential applications. This thesis aims to present a simulation of the Morris water maze using a robot in order to compare two different Reinforcement Learning techniques; model-based, where the transition function between each state is calculated during the interaction with the environment, and model-free, without a fully specified model of the environment. It will provide an overview of both principles and algorithms that can be used for Machine Learning in order to simulate animal behaviour, their advantages and disadvantages. A platform will be created to easily determine the best algorithm in both techniques. During the experiment, the robot will produce learning behaviour in order to be able to self-localise in his environment.

  @mastersthesis{mastersthesis,
    author       = {Victor B. F. Gomes}, 
    title        = {Controllers for Navigation using Reinforcement Learning},
    school       = {University of Sheffield and {INSA} Lyon},
    year         = 2012
  }
  




---

Teaching

Part II project (Cambridge)

• Michael Rawson, Part II Cambridge Computer Science Tripos project supervision with Dominic Mulligan. Project title: Verified metatheory and type checking for the simply-typed lambda calculus.


• Cristina Matache, Part II Cambridge Computer Science Tripos project supervision. Project title: Formalisation of the lambda-mu-T calculus in Isabelle/HOL.



Supervisions (Cambridge)

Michaelmas Term 16/17

• - Semantics of Programming Languages.
• - Discrete Mathematics.



Easter Term 15/16

• - Concepts in Programming Languages.



Demonstrations (Sheffield)

2013 - 2015

• - Foundations of Computer Science.
• - Automata, Logic and Computation.
• - Software Hut.
• - Software and Hardware Verification.




---

©2016 Victor Gomes - victor.gomes@cl.cam.ac.uk