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:20260522T150118Z
LOCATION:D171
DTSTART;TZID=America/Chicago:20181112T103000
DTEND;TZID=America/Chicago:20181112T105000
UID:submissions.supercomputing.org_SC18_sess150_ws_corr103@linklings.com
SUMMARY:Hybrid Theorem Proving as a Lightweight Method for Verifying Numer
 ical Software
DESCRIPTION:Alper Altuntas (National Center for Atmospheric Research) and 
 John Baugh (North Carolina State University)\n\nLarge-scale numerical soft
 ware requires substantial computer resources that complicate testing and d
 ebugging.  A single run of a climate model may require many millions of co
 re-hours and terabytes of disk space, making trial-and-error experiments b
 urdensome and time consuming.  In this study, we apply hybrid theorem prov
 ing from the field of cyber-physical systems to problems in scientific com
 putation, and show how to verify the correctness of discrete updates that 
 appear in the simulation of continuous physical systems.  By viewing numer
 ical software as a hybrid system that combines discrete and continuous beh
 avior, test coverage and confidence in findings can be increased.  We desc
 ribe abstraction approaches for modeling numerical software and demonstrat
 e the applicability of the approach in a case study that reproduces undesi
 rable behavior encountered in a parameterization scheme, called the K-prof
 ile parameterization, widely used in ocean components of large-scale clima
 te models.  We then identify and model a fix in the configuration of the s
 cheme, and verify that the undesired behavior is eliminated for all possib
 le execution sequences.  We conclude that hybrid theorem proving is an eff
 ective and efficient approach that can be used to verify and reason about 
 properties of large-scale numerical software.\n\nTag: Applications, Correc
 tness, Debugging, Floating Point, MPI, OpenMP, Runtime Systems, Tools, Ver
 ification\n\nRegistration Category: Workshop Reg Pass\n\nSession Chairs: I
 gnacio Laguna (Lawrence Livermore National Laboratory (LLNL)) and Cindy Ru
 bio-González (University of California, Davis)\n\n
END:VEVENT
END:VCALENDAR