BEGIN:VCALENDAR
PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN
CALSCALE:GREGORIAN
X-WR-CALNAME:Calagator
METHOD:PUBLISH
VERSION:2.0
BEGIN:VTIMEZONE
TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles
BEGIN:STANDARD
DTSTART:20111106T020000
RDATE:20111106T020000
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20120201T015730Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120206T110000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20120206T100000
DTSTAMP;VALUE=DATE-TIME:20120201T015730Z
LAST-MODIFIED;VALUE=DATE-TIME:20120201T015730Z
UID:http://calagator.org/events/1250461916
DESCRIPTION:Presented by Alan Mishchenko.\n\nLast spring\, in March 2010\
 , Aaron Bradley published the first truly new bit-level symbolic model c
 hecking algorithm since Ken McMillan’s interpolation based model check
 ing procedure introduced in 2003. Our experience with the algorithm sugg
 ests that it is stronger than interpolation on industrial problems\, and
  that it is an important algorithm to study further. In this paper\, we 
 present a simplified and faster implementation of Bradley’s procedure\
 , and discuss our successful and unsuccessful attempts to improve it.\n\
 nTags: galois\, formal methods\, tech talk\, model checking\n\nImported 
 from: http://calagator.org/events/1250461916
URL:http://corp.galois.com/blog/2012/1/31/tech-talk-efficient-implementat
 ion-of-property-directed-reac.html
SUMMARY:Galois Tech Talk: Efficient Implementation of Property Directed R
 eachability
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
END:VCALENDAR