Copyrights to these papers may be held by the publishers. The download files are preprints. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

N. Zhang and Franz Franchetti (Proc. Programming Languages Design and Implementation (PLDI), 2026)
Semantics Lifting for Scientific Kernels
Comment: 3rd Place in ACM Student Research Competition
Preprint (540 KB)
Bibtex

Modern compiler and code generation systems excel at lowering high-level specifications to optimized implementations. In contrast, the reverse direction, recovering high-level semantics from low- level code, remains relatively unexplored. This reverse direction, which can be viewed as semantics lifting, would enable verification and re-optimization of both generated and legacy code. Although lifting is undecidable in general, many scientific kernels exhibit strong mathematical structure that makes the problem tractable. We present an automatic semantics lifting framework built on SPIRAL, a mathematically grounded code generation system, for structured scientific kernels. By reversing SPIRAL’s code generation passes, our approach lifts source code through successive abstraction layers to recover its mathematical semantics. We implement a fully automated lifting pipeline and evaluate it on GPT-generated fast Fourier transform kernels, successfully recovering the transform specification and detecting semantic errors

Keywords:
Semantics lifting, Scientific kernels