CITATION — REFERENCE ENTRY
Towards Semantics Lifting for Scientific Computing: A Case Study on FFT — ACM
- Key
- zhang2025fft
- Authors
- Zhang, Naifeng; Rao, Sanil; Franusich, Mike; Franchetti, Franz
- Issued
- 2025-1-21
- Type
- paper-conference
- Publisher
- ACM
Raw CSL JSON
{
"URL": "https://users.ece.cmu.edu/~franzf/papers/2025_TPSA_Lifting.pdf",
"type": "paper-conference",
"title": "Towards Semantics Lifting for Scientific Computing: A Case Study on FFT",
"author": [
{
"given": "Naifeng",
"family": "Zhang"
},
{
"given": "Sanil",
"family": "Rao"
},
{
"given": "Mike",
"family": "Franusich"
},
{
"given": "Franz",
"family": "Franchetti"
}
],
"issued": {
"date-parts": [
[
2025,
1,
21
]
]
},
"publisher": "ACM",
"event-place": "Denver, CO, USA",
"event-title": "Workshop on Theory and Practice of Static Analysis (TPSA 2025), co-located with POPL 2025"
}
Claims
-
Stepwise semantics lifting reverses the code-generation (lowering) process: given a low-level scientific kernel, it applies a chain of inverse rewrites through intermediate representations (icode → Σ-SPL → SPL) to derive a high-level mathematical specification, with proof obligations discharged at each step.
"We propose to reverse the well-established code generation (i.e., lowering) process to stepwisely lift the semantics of the source code."
-
Semantic lifting is structured as a search problem: given a low-level implementation, the goal is to find a high-level specification together with a correctness witness establishing that the two are semantically equivalent.
"lifting is structured as a search problem, where each step identifies the sequence of rule applications necessary to increase the abstraction level"
-
LLM-generated scientific code may be syntactically valid but fall short of the correctness and performance standards required for complex scientific kernels, where numerical stability, domain-specific optimizations, and precise floating-point arithmetic are critical.
"Although LLM-generated code may be syntactically valid, it often falls short of meeting the rigorous correctness and performance standards required for complex scientific kernels."
-
Scientific computing poses unique challenges for static analysis, including accurate handling of floating-point arithmetic (rounding errors, numerical precision), pointer aliasing, recursion, and transcendental functions like sine and cosine.
"scientific computing poses unique challenges for static analysis tools. Accurate handling of floating-point arithmetic requires managing rounding errors and numerical precision, while pointers, recursion, and transcendental functions like sine and cosine further complicate static analysis."
-
SPIRAL's formal framework, built on the GAP computer algebra system, enables localized correctness checks during rule application between abstraction layers, verifying that each rewrite step preserves semantic equivalence.
"SPIRAL is built on top of the GAP computer algebra system, enabling localized correctness checks during rule application between abstraction layers."
Available in