enter search term and/or author name
Foreign function interfaces (FFIs) allow components in different languages to communicate directly with each other. While FFIs are useful, they often require writing tricky low-level code and include little or no static safety checking, thus...
Relations as an abstraction for BDD-based program analysis
Ondřej Lhoták, Laurie Hendren
Article No.: 19
In this article we present Jedd, a language extension to Java that supports a convenient way of programming with Binary Decision Diagrams (BDDs). The Jedd language abstracts BDDs as database-style relations and operations on relations, and...
Types for atomicity: Static checking and inference for Java
Cormac Flanagan, Stephen N. Freund, Marina Lifshin, Shaz Qadeer
Article No.: 20
Atomicity is a fundamental correctness property in multithreaded programs. A method is atomic if, for every execution, there is an equivalent serial execution in which the actions of the method are not interleaved with actions of other threads....
Java bytecode verification via static single assignment form
Andreas Gal, Christian W. Probst, Michael Franz
Article No.: 21
Java Virtual Machines (JVMs) traditionally perform bytecode verification by way of an iterative dataflow analysis. Bytecode verification is necessary to ensure type safety because temporary variables in the JVM are not statically typed. We present...
Remote specialization for efficient embedded operating systems
Sapan Bhatia, Charles Consel, Calton Pu
Article No.: 22
Prior to their deployment on an embedded system, operating systems are commonly tailored to reduce code size and improve runtime performance. Program specialization is a promising match for this process: it is predictable and modules, and it...
Register allocation for software pipelined multidimensional loops
Hongbo Rong, Alban Douillet, Guang R. Gao
Article No.: 23
This article investigates register allocation for software pipelined multidimensional loops where the execution of successive iterations from an n-dimensional loop is overlapped. For single loop software pipelining, the lifetimes of a loop...
We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We state semantically what is meant by correctness of a copying garbage collector, and employ a variant of the novel...