BEGIN:VCALENDAR
VERSION:2.0
PRODID:Linklings LLC
BEGIN:VTIMEZONE
TZID:America/Chicago
X-LIC-LOCATION:America/Chicago
BEGIN:DAYLIGHT
TZOFFSETFROM:-0600
TZOFFSETTO:-0500
TZNAME:CDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0500
TZOFFSETTO:-0600
TZNAME:CST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20181221T160728Z
LOCATION:D171
DTSTART;TZID=America/Chicago:20181112T155000
DTEND;TZID=America/Chicago:20181112T161000
UID:submissions.supercomputing.org_SC18_sess150_ws_corr109@linklings.com
SUMMARY:Toward Deductive Verification of Message-Passing Parallel Programs
DESCRIPTION:Workshop\nCorrectness, Debugging, MPI, Verification, Workshop 
 Reg Pass\n\nToward Deductive Verification of Message-Passing Parallel Prog
 rams\n\nLuo, Siegel\n\nProgram verification techniques based on deductive 
 reasoning can provide a very high level of assurance of correctness.  Thes
 e techniques are capable of proving correctness without placing artificial
  bounds on program parameters or on the sizes of inputs.  While there are 
 a number of mature frameworks for deductive verification of sequential pro
 grams, there is much less for parallel programs, and very little for messa
 ge-passing.  We propose a method for the deductive verification of message
 -passing programs that involves transforming the program into an annotated
  sequential program that can be verified with off-the-shelf deductive tool
 s, such as Frama-C.  The method can prove user-specified correctness prope
 rties without any bounds on the number of processes or other parameters.  
 We illustrate this method on a toy example, and analyze its strengths and 
 weaknesses.
URL:https://sc18.supercomputing.org/presentation/?id=ws_corr109&sess=sess1
 50
END:VEVENT
END:VCALENDAR