News – Research Institute in Automated Program Analysis and Verification https://verificationinstitute.org UK's Second Academic Research Institute in Cyber Security Wed, 10 Jun 2020 17:06:02 +0000 en-US hourly 1 RIAPAV to be succeeded by the Research Institute on Verified Trustworthy Software Systems (VeTSS) https://verificationinstitute.org/2017/03/ripav-to-be-succeeded-by-the-research-institute-on-verified-trustworthy-software-systems-vetss/ Fri, 10 Mar 2017 16:36:00 +0000 https://verificationinstitute.org/?p=1013 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 https://verificationinstitute.org/2016/05/talks-by-dana-scott-acm-a-m-turing-award-1976-thursday-26-may-friday-27th-may-and-wednesday-1-june/ Wed, 11 May 2016 15:40:36 +0000 https://verificationinstitute.org/?p=856 Read more »]]> 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

 

]]>
INVEST Workshop – December 2015 http://wp.doc.ic.ac.uk/verificationgroup/event/workshop-introduction-to-verification-and-testing-invest-2015/ Tue, 17 Nov 2015 12:21:41 +0000 https://verificationinstitute.org/?p=710 Verified Trustworthy Software Systems https://verificationinstitute.org/event/verified-trustworthy-software-systems-specialist-meeting/ Tue, 17 Nov 2015 12:09:42 +0000 https://verificationinstitute.org/?p=659 Annual Conference and Report, 2015 https://verificationinstitute.org/2015/09/uk-cyber-security-research-conference-2015/ Tue, 08 Sep 2015 09:51:38 +0000 https://verificationinstitute.org/?p=650 Read more »]]> 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)

]]>
FMATS4 at Microsoft Research, 2015 https://verificationinstitute.org/event/fourth-workshop-on-formal-methods-and-tools-for-security-fmats4/ Mon, 20 Apr 2015 15:09:43 +0000 https://verificationinstitute.org/?p=633 Institute’s Poster, 2014 https://verificationinstitute.org/2015/01/poster-presentation-at-the-ace-csrri-conference-december-2014/ Tue, 13 Jan 2015 10:36:19 +0000 https://verificationinstitute.org/?p=617 Download the Poster – Research Institute presented at the third ACE-CSR/RI Conference, December 16th 2014

]]>
INVEST Workshop – November 2014 http://wp.doc.ic.ac.uk/verificationgroup/event/workshop-introduction-to-verification/ Tue, 13 Jan 2015 10:29:25 +0000 https://verificationinstitute.org/?p=614 Annual Report, 2014 https://verificationinstitute.org/2015/01/1st-annual-report-2014/ Tue, 13 Jan 2015 10:20:44 +0000 https://verificationinstitute.org/?p=610 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)

]]>
Annual Conference, 2014 http://verificationinstitute.org/event/joint-annual-research-conference/ Mon, 28 Jul 2014 08:08:09 +0000 https://verificationinstitute.org/?p=573