@inproceedings{4816546bcd974a0ebe4bc366502fd4d5,
title = "C-2PO: A Weakly Relational Pointer Domain “These Are Not the Memory Cells You Are Looking For”",
abstract = "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.",
keywords = "abstract interpretation, pointers, static analysis, weakly relational domains",
author = "Rebecca Ghidini and Julian Erhard and Michael Schwarz and Helmut Seidl",
note = "Publisher Copyright: {\textcopyright} 2024 Copyright held by the owner/author(s).; 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains, NSAD 2024 ; Conference date: 22-10-2024",
year = "2024",
month = oct,
day = "17",
doi = "10.1145/3689609.3689994",
language = "English",
series = "NSAD 2024 - Proceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains, Co-located with SPLASH 2024",
publisher = "Association for Computing Machinery, Inc",
pages = "2--9",
editor = "Vincenzo Arceri and Michele Pasqua",
booktitle = "NSAD 2024 - Proceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains, Co-located with SPLASH 2024",
}