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:20260522T150119Z
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:Ziqing Luo and Stephen F. Siegel (University of Delaware)\n\nP
 rogram verification techniques based on deductive reasoning can provide a 
 very high level of assurance of correctness.  These techniques are capable
  of proving correctness without placing artificial bounds on program param
 eters or on the sizes of inputs.  While there are a number of mature frame
 works for deductive verification of sequential programs, there is much les
 s for parallel programs, and very little for message-passing.  We propose 
 a method for the deductive verification of message-passing programs that i
 nvolves transforming the program into an annotated sequential program that
  can be verified with off-the-shelf deductive tools, such as Frama-C.  The
  method can prove user-specified correctness properties without any bounds
  on the number of processes or other parameters.  We illustrate this metho
 d on a toy example, and analyze its strengths and weaknesses.\n\nTag: Appl
 ications, Correctness, Debugging, Floating Point, MPI, OpenMP, Runtime Sys
 tems, Tools, Verification\n\nRegistration Category: Workshop Reg Pass\n\nS
 ession Chairs: Ignacio Laguna (Lawrence Livermore National Laboratory (LLN
 L)) and Cindy Rubio-González (University of California, Davis)\n\n
END:VEVENT
END:VCALENDAR