BYU

Abstract by Jame Wasson

Personal Infomation


Presenter's Name

Jame Wasson

Degree Level

Undergraduate

Abstract Infomation


Department

Computer Science

Faculty Advisor

Eric Mercer

Title

Precise Pointer Arithmetic in Abstract Interpretation

Abstract

C is powerful because it gives programmers direct control over memory.

This control makes it the language of choice for many time- or memory-critical programs

but leads to subtle memory errors and undefined behaviors that often go unnoticed.

Not only is it useful to detect or disprove these errors, the ability to reason about these errors is a prerequisite to reasoning about other properties of C programs that use pointer arithmetic.

Pointer arithmetic has far-reaching effects but achieves them through very limited operations: addition and subtraction.

Additionally, memory can only be allocated in finite, discrete regions.

As a result, it is possible to create an abstract interpreter with an appropriately limited memory model that is faithful to these operations.

With the ability to reason about pointer arithmetic, it is also possible to reason about other properties of C.