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:20181221T160727Z
LOCATION:D171
DTSTART;TZID=America/Chicago:20181112T105000
DTEND;TZID=America/Chicago:20181112T111000
UID:submissions.supercomputing.org_SC18_sess150_ws_corr110@linklings.com
SUMMARY:HPC Software Verification in Action: A Case Study with Tensor Tran
 sposition
DESCRIPTION:Workshop\nApplications, Correctness, Debugging, Verification, 
 Workshop Reg Pass\n\nHPC Software Verification in Action: A Case Study wit
 h Tensor Transposition\n\nMutlu, Panyala, Krishnamoorthy\n\nAs HPC platfor
 ms get increasingly complex, the complexity of software optimized for thes
 e platforms has also increased. There is a pressing need to ensure correct
 ness of scientific applications to enhance our confidence in the results t
 hey produce. In this paper, we focus on checking the correctness of librar
 ies providing a small but important functionality---tensor transposition--
 -used in computational chemistry applications. While several correctness t
 ools have been developed and deployed, there are several practical challen
 ges in using them to verify production HPC software. We present our experi
 ences using two tools---CIVL and CodeThorn---in checking the correctness o
 f two index permutation libraries. We observe that, with some effort, the 
 tools we evaluated can handle kernels from production codes. We present ob
 servations that will aid library writers to write code that can be checked
  with these tools.
URL:https://sc18.supercomputing.org/presentation/?id=ws_corr110&sess=sess1
 50
END:VEVENT
END:VCALENDAR