Quantifying Hippocampal Shape Asymmetry in Alzheimer’s Disease Using Optimal Shape Correspondences
- Award ID(s):
- 2205417
- PAR ID:
- 10541976
- Publisher / Repository:
- IEEE
- Date Published:
- ISBN:
- 979-8-3503-1333-8
- Page Range / eLocation ID:
- 1 to 4
- Format(s):
- Medium: X
- Location:
- Athens, Greece
- Sponsoring Org:
- National Science Foundation
More Like this
-
Abstract Memory safety is a fundamental correctness property of software. For programs that manipulate linked, heap-allocated data structures, ensuring memory safety requires analyzing their possible shapes. Despite significant advances in shape analysis, existing techniques rely on hand-crafted domains tailored to specific data structures, making them difficult to generalize and extend. This paper presents a novel approach that reduces memory-safety proofs to the verification of heap-less imperative programs, enabling the use of off-the-shelf software verification tools. We achieve this reduction through two complementary program instrumentation techniques: space invariants, which enable symbolic reasoning about unbounded heaps, and flow abstraction, which encodes global heap properties as local flow equations. The approach effectively verifies memory safety across a broad range of programs, including concurrent lists and trees that lie beyond the reach of existing shape analysis tools.more » « less
An official website of the United States government

