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:20230124T171524Z
LOCATION:D167
DTSTART;TZID=America/Chicago:20221118T090000
DTEND;TZID=America/Chicago:20221118T092000
UID:submissions.supercomputing.org_SC22_sess448_ws_corr107@linklings.com
SUMMARY:Toward Verified Rounding-Error Analysis for Stationary Iterative M
ethods
DESCRIPTION:Workshop\n\nToward Verified Rounding-Error Analysis for Statio
nary Iterative Methods\n\nKellison, Tekriwal, Jeannin, Hulette\n\nIterativ
e methods for solving linear systems serve as a basic building block for c
omputational science. The computational cost of these methods can be signi
ficantly influenced by the round-off errors that accumulate as a result of
their implementation in finite precision. In the extreme case, round-off
errors that occur in practice can completely prevent an implementation fro
m satisfying the accuracy and convergence behavior prescribed by its under
lying algorithm. In the exascale era, where cost is paramount, a thorough
and rigorous analysis of the delay of convergence due to round-off should
not be ignored. In this paper, we use a small model problem and the Jacobi
iterative method to demonstrate how the Coq proof assistant can be used t
o formally specify the floating-point behavior of iterative methods, and t
o rigorously prove the accuracy of these methods.\n\nSession Format: Recor
ded\n\nTag: Correctness, Software Engineering\n\nRegistration Category: Wo
rkshop Reg Pass
END:VEVENT
END:VCALENDAR