RIAPAV to be succeeded by the Research Institute on Verified Trustworthy Software Systems (VeTSS)

The EPSRC will fund the the new Research Institute on Verified Trustworthy Software Systems (VeTSS) at Imperial for five years,  2017-2022.

The main purpose of VeTSS is to support program analysis, testing and verification, bringing together academics, industrialists and government employees to achieve guarantees of software correctness, safety, and security.

Talks by Dana Scott, ACM A.M. Turing award 1976, Thursday 26 May, Friday 27th May and Wednesday 1 June

Dana Scott, ACM A.M. Turing award 1976, gave a very well attended talk at Imperial on Stochastic λ-Calculus on Thursday 26th of May. The talk and lecture were part of a series of talks by Dana Scott in London in May and June, listed below.

Stochastic λ-Calculus. Thursday 26 May, Imperial College London.

Abstract: It is shown how the operators in the “graph model” for λ-calculus (which can function as a programming language for Recursive Function Theory) can be expanded to allow for “random combinators”.  The result then is a semantics for a new language for random algorithms.  The author wants to make a plea for finding applications.


Lambda Calculus: Then & Now. Thursday 26 May 2016, British Computer Society, London

Abstract: A very fast development in the early 1930’s following Hilbert’s codification of Mathematical Logic led to the Incompleteness Theorems, Computable Functions, Undecidability Theorems, and the general formulation of Recursive Function Theory. The so-called Lambda Calculus played a key role. The history of these developments will be traced, and the much later place of Lambda Calculus in Mathematics and Programming-Language Theory will be outlined.

Types and Type-free Lambda Calculus Friday 27th May, University College London

Abstract:  Denotational semantics started in Oxford in late 1969. It was hoped that domain theory would provide a basis both for recursive definitions in programs and recursive definitions of semantical structures. Early troubles were encountered in using tops and bottoms, and soon researchers turned to operational semantics. Others wanted to expand work to communicating and parallel processes. Axiomatic and synthetic theories did not solve the problems, and as a result much research effort in domain theory faded. Late work by Reynolds and collaborators, however, has opened up new and promising approaches for programming-language semantics. Perhaps the much simplified modeling using enumeration operators can spark some new investigations, especially since it is so easy to add a rich type structure to the calculus.

Why Mathematical Proof? Joint Maths Colloquium/EECS Distinguished seminar by Prof. Dana ScottWednesday 1 June, Queen Mary University of London, London


Annual Conference and Report, 2015

The Three National Cyber Security Programme sponsored cyber security Research Institutes are organising their joint annual highlights conference, at the Department for Business Innovation and Skills in October 2015. The purpose of the conference is to present this leading edge initiative and its outcomes to decision-makers and leaders from academia, government and industry.

Download the Annual report 2015 (PDF)

Annual Report, 2014

The Research Institute in Automated Program Analysis and Verification Annual Report provides an overview of the developments and achievements in 2014, our first year of operation.

Download the Annual report 2014 (PDF)