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:20181221T160906Z
LOCATION:D171
DTSTART;TZID=America/Chicago:20181112T090000
DTEND;TZID=America/Chicago:20181112T173000
UID:submissions.supercomputing.org_SC18_sess150@linklings.com
SUMMARY:2nd International Workshop on Software Correctness for HPC Applica
 tions (Correctness 2018)
DESCRIPTION:Workshop\nCorrectness, Debugging, Verification, Workshop Reg P
 ass\n\nIntroduction - 2nd International Workshop on Software Correctness f
 or HPC Applications (Correctness 2018)\n\nLaguna, Rubio-González\n\nEnsuri
 ng the correctness of high-performance computing (HPC) applications is one
  of the fundamental challenges that developers and users of these applicat
 ions face today. An application is correct when it performs what a user ex
 pects with respect to a specification. Given today's complex HPC softwar..
 .\n\n---------------------\nHybrid Theorem Proving as a Lightweight Method
  for Verifying Numerical Software\n\nAltuntas, Baugh\n\nLarge-scale numeri
 cal software requires substantial computer resources that complicate testi
 ng and debugging.  A single run of a climate model may require many millio
 ns of core-hours and terabytes of disk space, making trial-and-error exper
 iments burdensome and time consuming.  In this study, we app...\n\n-------
 --------------\nPARCOACH Extension for a Full-Interprocedural Collectives 
 Verification\n\nSaillard, Huchant, Barthou, Brunie, Carribault\n\nThe adve
 nt to exascale requires more scalable and efficient techniques to help dev
 elopers to locate, analyze and correct errors in parallel applications.\nP
 ARallel COntrol flow Anomaly CHecker (PARCOACH) is a framework that detect
 s the origin of collective errors in applications using MPI and/or Open...
 \n\n---------------------\nVerifying Qthreads: Is Model Checking Viable fo
 r User Level Tasking Runtimes?\n\nEvans\n\nThis paper describes a formal s
 pecification and verification of an HPC runtime through the design, implem
 en- tation and evaluation of a model checked implementation of the Qthread
 s many task runtime. We implement our model in Promela by doing a function
  to function translation of Qthreads’ C impleme...\n\n--------------------
 -\nUsing Polyhedral Analysis to Verify OpenMP Applications Are Data Race F
 ree\n\nYe, Schordan, Liao, Lin, Karlin...\n\nAmong the most common and har
 dest to debug types of bugs in concurrent systems are data races. In this 
 paper, we present an approach for verifying that an OpenMP program is data
  race free. We use polyhedral analysis to verify those parts of the progra
 m where we detect parallel affine loop nests. We ...\n\n------------------
 ---\nIncremental Static Race Detection in OpenMP Programs\n\nSwain, Huang\
 n\nOpenMP is a high level API that allows programmers to write concurrent 
 programs on multi-core systems. OpenMP provides an interface for easily ma
 naging teams of threads and concurrent tasks allowing the programmer to fo
 cus on modeling a problem concurrently rather than dealing with low level 
 thread ...\n\n---------------------\nCorrectness of Dynamic Dependence Ana
 lysis for Implicitly Parallel Tasking Systems\n\nLee, Stelle, McCormick, A
 iken\n\nIn this paper, we formally verify the correctness of dynamic depen
 dence analysis, a key algorithm for parallelizing programs in implicitly p
 arallel tasking systems. A dynamic dependence analysis of a program result
 s in a task graph, a DAG of tasks constraining the order of task execution
 . Because a ...\n\n---------------------\nToward Deductive Verification of
  Message-Passing Parallel Programs\n\nLuo, Siegel\n\nProgram verification 
 techniques based on deductive reasoning can provide a very high level of a
 ssurance of correctness.  These techniques are capable of proving correctn
 ess without placing artificial bounds on program parameters or on the size
 s of inputs.  While there are a number of mature framewor...\n\n----------
 -----------\nMaking Formal Methods for HPC Disappear\n\nGopalakrishnan\n\n
 Formal methods include rigorous specification methods that can render lang
 uage standards reliable and unambiguous. They also include rigorous testin
 g methods that target well-specified coverage criteria, and formal concept
 s that help guide debugging tool implementations. Those who say formal met
 hods...\n\n---------------------\nCorrectness of Floating Point Programs -
  Exception Handling and Reproducibility\n\nDemmel\n\nWe consider two relat
 ed aspects of analyzing and guaranteeing correctness of floating point pro
 grams: exception handling and reproducibility. Exception handling refers t
 o reliable and consistent propagation of errors due to overflow, invalid o
 perations (like sqrt(-1)), convergence failures, etc. Rep...\n\n----------
 -----------\nCompiler-Aided Type Tracking for Correctness Checking of MPI 
 Applications\n\nHück, Lehr\n\nMUST, a dynamic MPI correctness checker, is 
 extended with a type and memory allocation tracking sanitizer called TypeA
 RT for C/C++ codes based on the LLVM compiler framework.  The sanitizer ex
 tracts type information and inserts instrumentation to track memory alloca
 tions and deallocations relevant t...\n\n---------------------\nHPC Softwa
 re Verification in Action: A Case Study with Tensor Transposition\n\nMutlu
 , Panyala, Krishnamoorthy\n\nAs HPC platforms get increasingly complex, th
 e complexity of software optimized for these platforms has also increased.
  There is a pressing need to ensure correctness of scientific applications
  to enhance our confidence in the results they produce. In this paper, we 
 focus on checking the correctness...\n\n---------------------\nFacilitatin
 g the Adoption of Correctness Tools in HPC Applications\n\n\n\nThis open p
 anel will discuss Facilitating the Adoption of Correctness Tools in HPC Ap
 plications.\n\n---------------------\nWorkshop Lunch (on your own)\n\n\n\n
 Lunch on your own\n\n---------------------\nWorkshop Afternoon Break\n\n\n
 \n---------------------\nWorkshop Morning Break\n\n\n
END:VEVENT
END:VCALENDAR