Scalability is a key challenge in static analysis. For imperative languages like C, the approach taken for modeling memory can play a significant role in scalability. In this paper, we explore a family of memory models called partitioned memory models which divide memory up based on the results of a points-to analysis. We review Steensgaard’s original and field-sensitive points-to analyses and Data Structure Analysis (DSA), and introduce a new cell-based points-to analysis which further extends the benefit of field-sensitive analysis to heap data structures and type-unsafe operations like pointer arithmetics and pointer casting. We give experimental results on benchmarks from the software verification competition using the program verification framework in Cascade. We show that the partitioned memory model built on the cell-based points-to analysis significantly reduces the verification time for programs compared with models built on other analyses.
Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00
|Partitioned Memory Models for Program Analysis.
|Property Directed Reachability for Proving Absence of Concurrent Modification Errors
Asya Frumkin Tel Aviv University, Yotam M. Y. Feldman Tel Aviv University, Ondřej Lhoták University of Waterloo, Canada, Oded Padon Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv universityFile Attached
|Stabilizing Floating-Point Programs using Provenance Analysis