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:DAYLIGHT
DTSTART:20100314T020000
RDATE:20100314T020000
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20100727T184602Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100803T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20100803T103000
DTSTAMP;VALUE=DATE-TIME:20100727T184602Z
LAST-MODIFIED;VALUE=DATE-TIME:20100727T184602Z
UID:http://calagator.org/events/1250458930
DESCRIPTION:Galois is pleased to host the following tech talk.  These tal
 ks are open to the interested public.  Please join us!&#13\;\n&#13\;\nti
 tle:&#13\;\n    Industrial Strength Distributed Explicit Model Checking&
 #13\;\n&#13\;\npresenter:&#13\;\n    John Erickson&#13\;\n&#13\;\ntime:&
 #13\;\n    10:30am\,  August 3rd\, 2010&#13\;\n&#13\;\nlocation:&#13\;\n
     Galois Inc.&#13\;\n    421 SW 6th Ave. Suite 300\, Portland\, OR\, U
 SA&#13\;\n    (3rd floor of the Commonwealth building) &#13\;\n&#13\;\nA
 bstract:&#13\;\n    We present PReach\, an industrial strength distribut
 ed explicit state model checker based on Murphi. The goal of this projec
 t was to develop a reliable\, easy to maintain\, scalable model checker 
 that was compatible with the Murphi specification language. PReach is im
 plemented in the concurrent functional language Erlang\, chosen for its 
 parallel programming elegance. We use the original Murphi front-end to p
 arse the model description\, a layer written in Erlang to handle the com
 munication aspects of the algorithm\, and also use Murphi as a back-end 
 for state expansion and to store the hash table. This allowed a clean an
 d simple implementation\, with the core parallel algorithms written in u
 nder 1000 lines of code. This talk describes the PReach implementation i
 ncluding the various features that are necessary for the large models we
  target. We have used PReach to model check an industrial cache coherenc
 e protocol with approximately 30 billion states. To our knowledge\, this
  is the largest number published for a distributed explicit state model 
 checker. PReach has been released to the public under an open source BSD
  license.&#13\;\n&#13\;\nbio:&#13\;\n    John Erickson is a Design Engin
 eer at Intel Hillsboro.  He graduated with his PhD in Computer Science f
 rom The University of Texas at Austin in 2008.  Currently he is working 
 on the validation of uncore components in a 50+ core processor using a v
 ariety of formal and dynamic techniques. Past research interests include
  theorem proving with a focus on lemma generation and generalization in 
 the context of induction. \n\nImported from: http://calagator.org/events
 /1250458930
URL:http://www.galois.com/blog/2010/07/27/industrial-strength-distributed
 -explicit-model-checking/
SUMMARY:Galois Tech Talk
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
END:VCALENDAR