Dissertation/Thesis Abstract

Partition Memory Models for Program Analysis
by Wang, Wei, Ph.D., New York University, 2016, 137; 10025665
Abstract (Summary)

Scalability is a key challenge in static program analyses based on solvers for Satisability Modulo Theories (SMT). For imperative languages like C, the approach taken for modeling memory can play a significant role in scalability. The main theme of this thesis is using partitioned memory models to divide up memory based on the alias information derived from a points-to analysis.

First, a general analysis framework based on memory partitioning is presented. It incorporates a points-to analysis as a preprocessing step to determine a conservative approximation of which areas of memory may alias or overlap and splits the memory into distinct arrays for each of these areas.

Then we propose a new cell-based field-sensitive points-to analysis, which is an extension of Steensgaard's unification-based algorithms. A cell is a unit of access with scalar or record type. Arrays and dynamically memory allocations are viewed as a collection of cells. We show how our points-to analysis yields more precise alias information for programs with complex heap data structures.

Our work is implemented in Cascade, a static analysis framework for C programs. It replaces the former flat memory model that models the memory as a single array of bytes. We show that the partitioned memory models achieve better scalability within Cascade, and the cell-based memory model, in particular, improves the performance significantly, making Cascade a state-of-the-art C analyzer.

Indexing (document details)
Advisor: Barrett, Clark
Commitee: Goldberg, Benjamin, Ivancic, Franjo, Schwartz-Narbonne, Daniel, Wies, Thomas
School: New York University
Department: Computer Science
School Location: United States -- New York
Source: DAI-B 77/07(E), Dissertation Abstracts International
Source Type: DISSERTATION
Subjects: Computer science
Keywords: Memory model, Points-to analysis, SMT solver, Static analysis, Symbolic execution
Publication Number: 10025665
ISBN: 9781339521213
Copyright © 2019 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy
ProQuest