BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:jStar: Towards Practical Verification for Java - Matthew Parkinson
  (University of Cambridge)
DTSTART:20091201T130000Z
DTEND:20091201T140000Z
UID:TALK19692@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:In this talk\, we introduce a methodology for verifying some J
 ava programs which builds on recent theoretical\ndevelopments in program v
 erification: it combines the idea of abstract predicate families and the i
 dea of symbolic execution and abstraction using separation logic. The prop
 osed technology has been implemented in an automatic verification system\,
  called jStar\, which combines theorem proving and abstract interpretation
 \ntechniques.\n\nI will give an overview of the tool and a demo on an exam
 ple of the Visitor pattern.  I will also discuss the current weaknesses of
  the tool and discuss future directions to address these.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR