BEGIN:VCALENDAR
VERSION:2.0
PRODID:Linklings LLC
BEGIN:VTIMEZONE
TZID:America/New_York
X-LIC-LOCATION:America/New_York
BEGIN:DAYLIGHT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
TZNAME:EDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
TZNAME:EST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20250626T233532Z
LOCATION:B302-B305
DTSTART;TZID=America/New_York:20241121T100000
DTEND;TZID=America/New_York:20241121T170000
UID:submissions.supercomputing.org_SC24_sess534_post184@linklings.com
SUMMARY:Formal Approaches to Characterize Emerging Arithmetic Realizations
DESCRIPTION:Paul Jiang (Purdue University) and Iana Lin (University of Cal
 ifornia, Berkeley)\n\nAs HPC models grow increasingly complex, disparities
  in floating point implementations across hardware platforms begin to pose
  significant challenges to reproducibility and reliability. This is especi
 ally so, given that HPC employs hardware optimized for performance, which 
 quite often deviates from the IEEE Standard. We leverage SMT solvers, part
 icularly Z3, to develop a rigorous framework for analyzing and verifying t
 he behavior of computer arithmetic implementations in emerging hardware re
 alizations. Using bit-vectors to model IEEE non-standard behaviors, we are
  able to formally reason about intricate deviations in areas such as round
 ing rules, subnormal number handling, precision, normalization, etc. We de
 monstrate the framework's utility in two key applications: automating feat
 ure-targeted hardware testing for undocumented features and uncovering the
  degree of conformance to deeper properties such as monotonicity within th
 ese non-standard arithmetics. Our work also directly benefits cutting-edge
  GPU implementations, which is a timely issue underlying trust in scientif
 ic computation.\n\nRegistration Category: Tech Program Reg Pass, Exhibits 
 Reg Pass\n\nSession Chairs: Ayesha Afzal (Friedrich-Alexander University, 
 Erlangen-Nuremberg; Erlangen National High Performance Computing Center); 
 Sally Ellingson (University of Kentucky); and Alan Sussman (University of 
 Maryland)\n\n
END:VEVENT
END:VCALENDAR