Extending and compressing SVA
Bill Roscoe ( Oxford University Computing Laboratory )
- 11:30 11th March 2009 ( week 8, Hilary Term 2009 )Lecture Theatre A, Oxford University Computing Laboratory
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.
Share this:
