BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A monadic approach to automated reasoning for Bluespec SystemVeril
 og - Dominic Richards\, The University of Manchester
DTSTART:20110720T100000Z
DTEND:20110720T110000Z
UID:TALK32138@talks.cam.ac.uk
CONTACT:Jonathan Anderson
DESCRIPTION:A non-trivial subset of Bluespec SystemVerilog (BSV) is embedd
 ed in the higher order logic of the PVS theorem prover. Owing to the clean
  semantics of BSV\, application of monadic techniques leads to a surprisin
 gly elegant embedding\, in which hardware designs are translated into logi
 c almost verbatim\, preserving types and language constructs. The resultin
 g specifications are compatible with the built-in model checker of PVS\, w
 hich can automatically prove an important class of temporal logic theorems
 \, and can also be used in conjunction with the powerful proof strategies 
 of PVS\, including automatic predicate abstraction\, to verify a broader c
 lass of properties than can be achieved with model checking alone. Further
 more\, the above BSV subset is also embedded in the specification language
  of the SAL model checker\, which provides a diverse array of fully-automa
 ted verification techniques.\n\nBluespec SystemVerilog is a hardware descr
 iption language based on the guarded action model of concurrency. It has a
 n elegant semantics\, which has previously been shown to support design ve
 rification by hand proof: to date\, however\, little work has been conduct
 ed on the application of automated reasoning to BSV designs.
LOCATION:Lecture Theatre 2\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR