Tue 22 Oct 2024 14:30 - 15:00 at Pacific B - NSAD: Session 2 Chair(s): Thomas P. Jensen

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 Oct

Displayed time zone: Pacific Time (US & Canada) change

14:00 - 15:30
NSAD: Session 2NSAD at Pacific B
Chair(s): Thomas P. Jensen INRIA Rennes
14:00
30m
Full-paper
A Step-Function Abstract Domain for Granular Floating-Point Error AnalysisFull Paper
NSAD
Anthony Dario University of Oregon, Samuel D. Pollard Sandia National Laboratories
DOI
14:30
30m
Full-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
30m
Full-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