victor.gomes@cl.cam.ac.uk
University of Cambridge
Computer Laboratory
William Gates Building
15 JJ Thomson Avenue
Cambridge CB3 0FD, UK
My publications are also available on DBLP.
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}
}
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}
}
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}
}
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}
}
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}
}
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}
}
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}
}
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}
}
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}
}
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}
}
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
}
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
}
©2016 Victor Gomes - victor.gomes@cl.cam.ac.uk