enter search term and/or author name
A uniform type structure for secure information flow
Kohei Honda, Nobuko Yoshida
Article No.: 31
The π-calculus, a calculus of mobile processes, can compositionally represent dynamics of major programming constructs by decomposing them into name passing. The present work reports our experience in using a linear/affine typed π-calculus...
Object-oriented languages provide little support for encapsulating objects. Reference semantics allows objects to escape their defining scope, and the pervasive aliasing that ensues remains a major source of software defects. This paper presents...
The embedded machine: Predictable, portable real-time code
Thomas A. Henzinger, Christoph M. Kirsch
Article No.: 33
The Embedded Machine is a virtual machine that mediates in real time the interaction between software processes and physical processes. It separates the compilation of embedded programs into two phases. The first phase, the platform-independent...
A step towards unifying schedule and storage optimization
William Thies, Frédéric Vivien, Saman Amarasinghe
Article No.: 34
We present a unified mathematical framework for analyzing the tradeoffs between parallelism and storage allocation within a parallelizing compiler. Using this framework, we show how to find a good storage mapping for a given schedule, a good...
Fingerprinting embeds a secret message into a cover message. In media fingerprinting, the secret is usually a copyright notice and the cover a digital image. Fingerprinting an object discourages intellectual property theft, or when such theft has...
This article develops a proof theory for low-level code languages. We first define a proof system, which we refer to as the sequential sequent calculus, and show that it enjoys the cut elimination property and that its expressive power is...
Optimizing indirect branch prediction accuracy in virtual machine interpreters
Kevin Casey, M. Anton Ertl, David Gregg
Article No.: 37
Interpreters designed for efficiency execute a huge number of indirect branches and can spend more than half of the execution time in indirect branch mispredictions. Branch target buffers (BTBs) are the most widely available form of indirect...
An improved bound for call strings based interprocedural analysis of bit vector frameworks
Bageshri Karkare, Uday P. Khedker
Article No.: 38
Interprocedural data flow analysis extends the scope of analysis across procedure boundaries in search of increased optimization opportunities. Call strings based approach is a general approach for performing flow and context sensitive...
Goal-directed weakening of abstract interpretation results
Sunae Seo, Hongseok Yang, Kwangkeun Yi, Taisook Han
Article No.: 39
One proposal for automatic construction of proofs about programs is to combine Hoare logic and abstract interpretation. Constructing proofs is in Hoare logic. Discovering programs' invariants is done by abstract interpreters.
One problem of...