Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis

Helmut Seidl18 Contact Information, Vesal Vojdani18 Contact Information and Varmo Vene19 Contact Information

(18)  Lehrstuhl für Informatik II, Technische Universität München, Boltzmannstraße 3, D-85748 Garching b. München, Germany
(19)  Deptartment of Computer Science, University of Tartu, J. Liivi 2, EE-50409 Tartu, Estonia
Abstract
We present a new domain for analyzing must-equalities between address expressions. The domain is a smooth combination of Herbrand and affine equalities which enables us to describe field accesses and array indexing. While the full combination of uninterpreted functions with affine arithmetics results in intractable assertion checking algorithms, our restricted domain allows us to construct an analysis of address must-equalities that runs in polynomial time. We indicate how this analysis can be applied to infer access patterns in programs manipulating arrays and structs.

Contact Information Helmut Seidl
Email: seidl@in.tum.de

Contact Information Vesal Vojdani
Email: vojdanig@in.tum.de

Contact Information Varmo Vene
Email: varmo@cs.ut.ee
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.111 • Server: mpweb07
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)