SPLASH 2024 (series) / NSAD 2024 (series) / NSAD 2024 / C-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are Looking For”
C-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are Looking For”Full Paper
Pointer analysis is foundational for statically analyzing real-world programs. We present C-2PO — a weakly relational domain for C programs, which tracks must-equalities and -disequalities between pointer expressions. This domain captures address arithmetic and its confinement to single memory objects, both core concepts in C. We implement the domain in Goblint
and provide a preliminary evaluation. For 95% of SV-COMP tasks, the slowdown incurred by adding C-2PO is below a factor of 3. To measure precision, we instrumented coreutil programs with assertions computed by C-2PO. For an existing non-relational pointer analysis, 80% of the assertions are out of reach.
Tue 22 OctDisplayed time zone: Pacific Time (US & Canada) change
Tue 22 Oct
Displayed time zone: Pacific Time (US & Canada) change
14:00 - 15:30 | |||
14:00 30mFull-paper | A Step-Function Abstract Domain for Granular Floating-Point Error AnalysisFull Paper NSAD DOI | ||
14:30 30mFull-paper | C-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are Looking For”Full Paper NSAD Rebecca Ghidini TU Munich, Julian Erhard LMU Munich; TU Munich, Michael Schwarz TU Munich, Helmut Seidl TU Munich DOI | ||
15:00 30mFull-paper | Stability: An Abstract Domain for the Trend of Variation of Numerical VariablesFull Paper NSAD Luca Negrini Ca’ Foscari University of Venice, Sofia Presotto Ca’ Foscari University of Venice, Pietro Ferrara Ca’ Foscari University of Venice, Enea Zaffanella University of Parma, Agostino Cortesi Ca’ Foscari University of Venice DOI |