LMS Computer Science Colloquium 2023

LMS Computer Science Colloquium 2023

The LMS Computer Science Colloquium is an annual event, which includes themed talks on a topical issue at the interface of mathematics and computer science.

The theme of this year's Colloquium is: Verification: Theory and Practice.

The Colloquium is organised by the LMS Computer Science Committee and is aimed at PhD students and post-docs, although others are welcome to attend, whether LMS members or not.

We will endeavour to upload the talks to the LMS YouTube channel - click 'subscribe' to be alerted when new videos are added.

Programme (all times in GMT)

Abstracts

Ana Cavalcanti (University of York) - Verification of control software for robots that learn
RoboStar is a centre of excellence on Software Engineering for Robotics; we are developing a collection of domain-specific notations to model various artefacts, and techniques for model-transformation, simulation, testing, and proof based on rigorous mathematical foundations. In this presentation, we describe our approach to (1) modelling artificial neural network (ANN) components as part of behavioural models for control software and (2) verification using traditional and ANN-specific verification tools. Existing techniques and tools for ANN verification are concerned with component-level properties. In RoboStar, we deal with properties that may depend on all software components. Our focus is on trained neural networks for control. Our proof approach is based on refinement and provides deductive guarantees on behaviour, so that ANNs can therefore be treated as reliable, white-box components.

Rod Chapman (Amazon Web Services) - Automated Reasoning at AWS, and Applications in Cryptography:
This talk will start with an overview of the uses of Automated Reasoning (AR) at AWS, with an emphasis on the technical and business drivers that have made for some notable successes within the business. I'd then like to turn to more specific challenges of developing and verifying cryptographic software and how AR applies in that domain.

Angeliki Koutsoukou-Argyraki (Royal Holloway, University of London) - Perspectives on the formalisation of mathematics: verification and beyond:
Formalising mathematics with interactive theorem provers, like Isabelle/HOL and Lean, has seen a significant increase in popularity in recent years, with flourishing formalisation communities attracting both computer scientists and mathematicians. While ensuring correctness is an important aspect of mathematical practice, formalising mathematics goes beyond the scope of verification. This talk will involve a brief discussion on the state of the art and the potential of the area.

Giles Reger (University of Manchester) - The Vampire Journey: building a theorem prover for program verification:
Vampire is a fully automated theorem prover for first-order logic that has been developed for over 25 years. It has a long tradition of being the “best” in the world (solves the most in the least time at the theorem prover competition) for traditional first-order logic problems found in many domains. However, this traditional first-order logic setting often struggles to capture problems from program verification that need to talk about theories such as arithmetic. Indeed, program verification is typically the domain of SMT solvers (Boolean SAT solvers extended with theory decision procedures). However, we often see problems in program verification that combine theories and quantification (the bread-and-butter of traditional first-order logic reasoning) where SMT solvers struggle with heuristic approaches. Therefore, around 10 years ago we embarked on a journey to extend Vampire to the program verification space, adding theory reasoning, induction, interpolation, and a some other fun things. It is this journey, the challenges, advances, and applications, that I will talk about in this presentation

Accessibility

The building currently has stepped access only to the raised ground floor and lower ground floor entrances.

An accessible toilet is located at the lower ground floor level.

Please see the LMS website for further details on accessibility

Registration

• To attend in person, please complete the registration form here.
   

• To attend remotely via Zoom, please complete the registration form here. Registration will close no later than 16:30 on Friday 1 December. You will receive the link to the meeting upon registration, as well as an automated reminder email sent 24 hours before the event is scheduled to start.
   

• Grants of up to £200 are available to parents and carers who wish to attend this event and require help towards caring costs. Please see the Caring Supplementary Grants page on the LMS website. Please submit your application no later than 15:00 on Friday 24 November. For any questions on Caring Grants, please contact caringgrants@lms.ac.uk.
   

• For all other queries, please contact lmscomputerscience@lms.ac.uk.