Tue 16 Jun 2026 16:35 - 16:55 at Meadows CD - HPC Programming

While formal verification techniques for evaluating correctness of complex algorithms such as deep neural networks (DNNs) have advanced over the years, enabling their use in safety-critical spaces such as healthcare, a significant gap remains when deploying these algorithms on embedded, resource constrained platforms: sound deployment is at odds with computational efficiencies, and numerical differences are breaking verification guarantees. First, software (SW) schemes designed for porting algorithms onto edge devices – such as quantization schemes – are either static and sound (non-optimal power consumption), or dynamic yet unsound (non-optimal for safety-critical applications). Second, hardware (HW) such as GPUs, NPUs and TPUs are designed for throughput rather than correctness of computation of security, and are as such susceptible to bit-flip attacks that can significantly alter functionality of deployed algorithms, ``silently'' breaking verification guarantees. To address both these needs we propose a both wholly new approach to real-time, dynamic and sound quantization, as well as the hardware to support it. First we developed a sound, real-time adaptive-precision quantization approach utilizing left-to-right arithmetic to pass the most significant bits (MSB) first, and dynamically adjust precision online while performing sensitivity analysis to quantify and manage the risk of decision-boundary crossings. Next, we propose a novel HW approach utilizing systolic arrays to perform left-to-right arithmetic to generate the MSB first. Together these provide a wholly novel framework for enabling not only resource-efficient neural networks and artificial intelligence at the edge, but broadly sound and resource-efficient high-precision mathematics on HW that ensures resilience to bit flip attacks on the most critical bits, and enabling carrying over of verification guarantees on algorithms from development to deployment. This work is presented as work-in-progress, with SW implementations completed and HW in-progress

Tue 16 Jun

Displayed time zone: Mountain Time (US & Canada) change

15:50 - 17:30
HPC ProgrammingARRAY at Meadows CD
15:50
20m
Talk
Vectorizing Sparse Coiteration for Two-finger Loop Structure (Extended Abstract)
ARRAY
Kabilan Mahathevan Virginia Tech, Kirshanthan Sundararajah Virginia Tech
16:10
25m
Talk
Leveraging AI Ecosystem for Portable and Sustainable GPU Kernels in HPC
ARRAY
Yanbo Zhao North Carolina State University, Zhaonan Meng North Carolina State University, Sai Krishna Teja Varma Manthena North Carolina State University, Xu Liu North Carolina State University, Ajay Panyala Pacific Northwest National Laboratory, Jiajia Li North Carolina State University
DOI
16:35
20m
Talk
Lazy Arithmetic using Systolic Arrays for Closing the Verification Gap on Embedded Systems
ARRAY
Taisa Kushner Galois, Ryan McCleeary Galois, Martin Brain City St. George's, University of London
16:55
20m
Talk
Towards a Linear-Algebraic Hypervisor
ARRAY
Pre-print
17:15
5m
Research preview
Semantics as a Tool of Thought: Provenance-Aware Dimensional Checking in a Reactive Array IR
ARRAY
17:20
10m
Live Q&A
Mini Panel
ARRAY