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: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:Workshop\nApplications, Correctness, Debugging, Verification, 
 Workshop Reg Pass\n\nHybrid Theorem Proving as a Lightweight Method for Ve
 rifying Numerical Software\n\nAltuntas, Baugh\n\nLarge-scale numerical sof
 tware requires substantial computer resources that complicate testing and 
 debugging.  A single run of a climate model may require many millions of c
 ore-hours and terabytes of disk space, making trial-and-error experiments 
 burdensome and time consuming.  In this study, we apply hybrid theorem pro
 ving from the field of cyber-physical systems to problems in scientific co
 mputation, and show how to verify the correctness of discrete updates that
  appear in the simulation of continuous physical systems.  By viewing nume
 rical software as a hybrid system that combines discrete and continuous be
 havior, test coverage and confidence in findings can be increased.  We des
 cribe abstraction approaches for modeling numerical software and demonstra
 te the applicability of the approach in a case study that reproduces undes
 irable behavior encountered in a parameterization scheme, called the K-pro
 file parameterization, widely used in ocean components of large-scale clim
 ate models.  We then identify and model a fix in the configuration of the 
 scheme, and verify that the undesired behavior is eliminated for all possi
 ble execution sequences.  We conclude that hybrid theorem proving is an ef
 fective and efficient approach that can be used to verify and reason about
  properties of large-scale numerical software.
URL:https://sc18.supercomputing.org/presentation/?id=ws_corr103&sess=sess1
 50
END:VEVENT
END:VCALENDAR