Skip to main content

Extending and compressing SVA

Bill Roscoe ( 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: