Logo

Giacomo Boldini

PhD Student
Ca' Foscari University of Venice

SSV Research Group

Modular Abstract Interpretation for Stack-Heap Analysis of C/C++ via LLVM IR

Authors: Giacomo Boldini
Student Research Competition @ SPLASH/ISSTA 2026 — Companion Proceedings of the 2026 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH Companion '26), ACM, pp. 42–44
Oakland, CA, USA, October 5, 2026
Extended abstract (ACM Student Research Competition)

Abstract

Detecting memory errors in C/C++ by static analysis means reasoning about program values and memory structure together, but value- and memory-oriented analyses are usually combined in fixed, domain-specific ways. This work proposes a modular, parametric framework, based on abstract interpretation theory, with a split-state abstraction that separates values from memory structure into two independent, interchangeable domains. Any pair satisfying a minimal interface yields a sound combined analysis by construction. Precision can thus be adapted without redesigning the analysis, for instance by trading a coarser memory domain for a richer value one.

Conference page: Link
ACM page: Link