PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Mon 16 Jun 2025 16:40 - 17:00 at Grand Ball Room 1 - AI and Accelerator Architecture + WIP

In the context of modern day embedded safety-critical systems and low-resource edge devices in particular, Sigma-Delta Neural Networks (SDNNs) offer a promising alternative to traditional Artificial Neural Networks (ANNs) by leveraging event-driven, sparse computations inspired by biological neural processing. This energy-efficient paradigm makes SDNNs well-suited for neuromorphic hardware and real-time applications, particularly in scenarios with temporal redundancy, such as video processing. However, as neural networks become integral to safety-critical systems, ensuring their robustness against adversarial perturbations is an absolute necessity. In this work, we propose an end-to-end framework for formal modeling and verification of SDNNs using Satisfiability Modulo Theory (SMT). Unlike empirical robustness evaluations, SMT-based verification provides formal guarantees by encoding SDNN behavior and adversarial robustness properties as mathematical constraints. We introduce an SMT-based formulation for encoding SDNNs with SMT constraints and define a robustness property motivated by video stream processing. Our approach systematically examines how well SDNNs can handle adversarial attacks, ensuring they work correctly in safety-critical applications. We validate our framework through experiments on temporal version of the MNIST dataset. To the best of our knowledge, this is the first formal verification framework for SDNNs, bridging the gap between neuromorphic computing and rigorous verification.

This program is tentative and subject to change.

Mon 16 Jun

Displayed time zone: Seoul change

15:40 - 17:20
AI and Accelerator Architecture + WIPLCTES at Grand Ball Room 1
15:40
20m
Talk
SPARQ: An Accelerator Architecture for Large Language Models with Joint Sparsity and Quantization Techniques
LCTES
Seonggyu Choi Sungkyunkwan University, Hyungmin Cho Sungkyunkwan University
DOI
16:00
20m
Talk
ADaPS: Adaptive Data Partitioning to Parallelize CNN Inference on Resource-Constrained Hardware
LCTES
Jaume Mateu Cuadrat Seoul National University, Bernhard Egger Seoul National University
DOI
16:20
20m
Talk
Graphitron: A Domain Specific Language for FPGA-Based Graph Processing Accelerator Generation
LCTES
Xinmiao Zhang SKLP, Institute of Computing Technology, CAS, Zheng Feng Institute of Computing Technology at Chinese Academy of Sciences, Shengwen Liang SKLP, Institute of Computing Technology, CAS, Xinyu Chen Hong Kong University of Science and Technology, Lei Zhang ICT CAS, Cheng Liu ICT CAS
DOI
16:40
20m
Talk
Modeling and Verification of Sigma Delta Neural Networks using Satisfiability Modulo Theory
LCTES
Sirshendu Das Indian Statistical Institute, Ansuman Banerjee Indian Statistical Institute, Swarup Kumar Mohalik Ericsson Research
DOI
17:00
10m
Talk
Zoozve: A Strip-Mining-Free RISC-V Vector Extension with Arbitrary Register Grouping Compilation Support (WIP)
LCTES
Siyi Xu Shanghai University, Limin Jiang Shanghai University, Yintao Liu Shanghai University, Yihao Shen Shanghai University, Yi Shi Shanghai University, Shan Cao Shanghai University, Zhiyuan Jiang Shanghai University
DOI
17:10
10m
Talk
Towards Macro-Aware C-to-Rust Transpilation (WIP)
LCTES
Robbe De Greef Vrije Universiteit Brussel, Attilio Discepoli Vrije Universiteit Brussel, Esteban Aguililla Klein Université Libre de Bruxelles, Théo Engels Royal Military Academy of Belgium, Ken Hasselmann Royal Military Academy of Belgium, Antonio Paolillo Vrije Universiteit Brussel
DOI