Extending and compressing SVA

Bill Roscoe (Oxford University Computing Laboratory)

Info

Date	11th March 2009 (week 8, Hilary Term 2009)
Time	11:30
Place	Lecture Theatre A, Oxford University Computing Laboratory

Abstract

SVA is a front end for FDR developed by Bill Roscoe and David Hopkins that allows the user to write shared variable programs, check properties of these on FDR, and have any examples reported in a user-friendly way.

In this talk I will discuss the structure of SVA and demonstrate its use on some examples — including an analysis of a fascinating open problem. I will then discuss new additions to the tool extending the input language to incorporate simple types and arrays with variable indices, and which use FDR's compression functions quite effectively.