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:20260522T150123Z
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:Making Formal Methods for HPC Disappear\n\nFormal methods incl
 ude rigorous specification methods that can render language standards reli
 able and unambiguous. They also include rigorous testing methods that targ
 et well-specified coverage criteria, and formal concepts that help guide d
 ebugging tool implementations. Those who say formal methods...\n\n\nGanesh
  L. Gopalakrishnan (University of Utah)\n---------------------\nIntroducti
 on - 2nd International Workshop on Software Correctness for HPC Applicatio
 ns (Correctness 2018)\n\nEnsuring the correctness of high-performance comp
 uting (HPC) applications is one of the fundamental challenges that develop
 ers and users of these applications face today. An application is correct 
 when it performs what a user expects with respect to a specification. Give
 n today's complex HPC softwar...\n\n\nIgnacio Laguna (Lawrence Livermore N
 ational Laboratory) and Cindy Rubio-González (University of California, Da
 vis)\n---------------------\nWorkshop Lunch (on your own)\n\nLunch on your
  own\n\n---------------------\nUsing Polyhedral Analysis to Verify OpenMP 
 Applications Are Data Race Free\n\nAmong the most common and hardest to de
 bug 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 program where we
  detect parallel affine loop nests. We ...\n\n\nFangke Ye (Georgia Institu
 te of Technology); Markus Schordan, Chunhua Liao, Pei-Hung Lin, and Ian Ka
 rlin (Lawrence Livermore National Laboratory); and Vivek Sarkar (Georgia I
 nstitute of Technology)\n---------------------\nWorkshop Morning Break\n--
 -------------------\nFacilitating the Adoption of Correctness Tools in HPC
  Applications\n\nThis open panel will discuss Facilitating the Adoption of
  Correctness Tools in HPC Applications.\n\n---------------------\nHPC Soft
 ware Verification in Action: A Case Study with Tensor Transposition\n\nAs 
 HPC platforms get increasingly complex, the complexity of software optimiz
 ed for these platforms has also increased. There is a pressing need to ens
 ure correctness of scientific applications to enhance our confidence in th
 e results they produce. In this paper, we focus on checking the correctnes
 s...\n\n\nErdal Mutlu, Ajay Panyala, and Sriram Krishnamoorthy (Pacific No
 rthwest National Laboratory)\n---------------------\nVerifying Qthreads: I
 s Model Checking Viable for User Level Tasking Runtimes?\n\nThis paper des
 cribes a formal specification and verification of an HPC runtime through t
 he design, implemen- tation and evaluation of a model checked implementati
 on of the Qthreads many task runtime. We implement our model in Promela by
  doing a function to function translation of Qthreads’ C impleme...\n\n\nN
 oah Evans (Sandia National Laboratories)\n---------------------\nIncrement
 al Static Race Detection in OpenMP Programs\n\nOpenMP is a high level API 
 that allows programmers to write concurrent programs on multi-core systems
 . OpenMP provides an interface for easily managing teams of threads and co
 ncurrent tasks allowing the programmer to focus on modeling a problem conc
 urrently rather than dealing with low level thread ...\n\n\nBradley Swain 
 and Jeff Huang (Texas A&M University)\n---------------------\nToward Deduc
 tive Verification of Message-Passing Parallel Programs\n\nProgram verifica
 tion techniques based on deductive reasoning can provide a very high level
  of assurance of correctness.  These techniques are capable of proving cor
 rectness without placing artificial bounds on program parameters or on the
  sizes of inputs.  While there are a number of mature framewor...\n\n\nZiq
 ing Luo and Stephen F. Siegel (University of Delaware)\n------------------
 ---\nCorrectness of Dynamic Dependence Analysis for Implicitly Parallel Ta
 sking Systems\n\nIn this paper, we formally verify the correctness of dyna
 mic dependence analysis, a key algorithm for parallelizing programs in imp
 licitly parallel tasking systems. A dynamic dependence analysis of a progr
 am results in a task graph, a DAG of tasks constraining the order of task 
 execution. Because a ...\n\n\nWonchan Lee (Stanford University), George St
 elle and Patrick McCormick (Los Alamos National Laboratory), and Alex Aike
 n (Stanford University)\n---------------------\nCorrectness of Floating Po
 int Programs - Exception Handling and Reproducibility\n\nWe consider two r
 elated aspects of analyzing and guaranteeing correctness of floating point
  programs: exception handling and reproducibility. Exception handling refe
 rs to reliable and consistent propagation of errors due to overflow, inval
 id operations (like sqrt(-1)), convergence failures, etc. Rep...\n\n\nJame
 s Demmel (University of California, Berkeley)\n---------------------\nWork
 shop Afternoon Break\n---------------------\nPARCOACH Extension for a Full
 -Interprocedural Collectives Verification\n\nThe advent to exascale requir
 es more scalable and efficient techniques to help developers to locate, an
 alyze and correct errors in parallel applications.\nPARallel COntrol flow 
 Anomaly CHecker (PARCOACH) is a framework that detects the origin of colle
 ctive errors in applications using MPI and/or Open...\n\n\nEmmanuelle Sail
 lard, Pierre Huchant, and Denis Barthou (French Institute for Research in 
 Computer Science and Automation (INRIA)) and Hugo Brunie and Patrick Carri
 bault (Atomic Energy and Alternative Energies Commission (CEA))\n---------
 ------------\nCompiler-Aided Type Tracking for Correctness Checking of MPI
  Applications\n\nMUST, a dynamic MPI correctness checker, is extended with
  a type and memory allocation tracking sanitizer called TypeART for C/C++ 
 codes based on the LLVM compiler framework.  The sanitizer extracts type i
 nformation and inserts instrumentation to track memory allocations and dea
 llocations relevant t...\n\n\nAlexander Hück and Jan-Patrick Lehr (Technic
 al University Darmstadt, Scientific Computing)\n---------------------\nHyb
 rid Theorem Proving as a Lightweight Method for Verifying Numerical Softwa
 re\n\nLarge-scale numerical software requires substantial computer resourc
 es that complicate testing and debugging.  A single run of a climate model
  may require many millions of core-hours and terabytes of disk space, maki
 ng trial-and-error experiments burdensome and time consuming.  In this stu
 dy, we app...\n\n\nAlper Altuntas (National Center for Atmospheric Researc
 h) and John Baugh (North Carolina State University)\n\nTag: Applications, 
 Correctness, Debugging, Floating Point, MPI, OpenMP, Runtime Systems, Tool
 s, Verification\n\nRegistration Category: Workshop Reg Pass\n\nSession Cha
 irs: Ignacio Laguna (Lawrence Livermore National Laboratory (LLNL)) and Ci
 ndy Rubio-González (University of California, Davis)
END:VEVENT
END:VCALENDAR