1,205 papers · page 16 of 61
Mobile computation, in which executing computations can move from one physical computing device to another, is a recurring theme: from OS process migration, to language-level mobility, to virtual machine migration. This article reports on the design, implementation, and verificat…
It is important to prove that supposedly terminating programs actually terminate, particularly if those programs must be run on critical systems or downloaded into a client such as a mobile phone. Although termination of computer programs is generally undecidable, it is possible …
Software-controlled scratchpad memory is increasingly employed in embedded systems as it offers better timing predictability compared to caches. Previous scratchpad allocation algorithms typically consider single-process applications. But embedded applications are mostly multitas…
With the commercial development of multicore processors, the challenges of writing multithreaded programs to take advantage of these new hardware architectures are becoming more and more pertinent. Concurrent programming is necessary to achieve the performance that the hardware o…
We provide a parametric framework for verifying safety properties of concurrent heap-manipulating programs. The framework combines thread-scheduling information with information about the shape of the heap. This leads to verification algorithms that are more precise than existing…
Modern embedded processors with dedicated address generation unit support memory accesses through auto-increment/decrement addressing mode. The auto-increment/decrement mode, if properly utilized, can save address arithmetic instructions, reduce static and dynamic memory footprin…
Recent work on adaptive functional programming (AFP) developed techniques for writing programs that can respond to modifications to their data by performing change propagation . To achieve this, executions of programs are represented with dynamic dependence graphs (DDGs) that rec…
We propose a sequent calculus derived from the λ―μμ˜-calculus of Curien and Herbelin that is expressive enough to directly represent the fine details of program evaluation using typical abstract machines. Not only does the calculus easily encode the usual components of abstract m…
Proof Carrying Code provides trust in mobile code by requiring certificates that ensure the code adherence to specific conditions. The prominent approach to generate certificates for compiled code is Certifying Compilation, that automatically generates certificates for simple saf…
An extension of the λ-calculus is proposed, to study resource usage analysis and verification. It features usage policies with a possibly nested, local scope, and dynamic creation of resources. We define a type and effect system that, given a program, extracts a history expressio…
Contracts are behavioral descriptions of Web services. We devise a theory of contracts that formalizes the compatibility of a client with a service, and the safe replacement of a service with another service. The use of contracts statically ensures the successful completion of ev…
Self-stabilization is an elegant approach for designing fault tolerant systems. A system is considered self-stabilizing if, starting in any state, it converges to the desired behavior. Self-stabilizing algorithms were designed for solving fundamental distributed tasks, such as le…
A dependence cluster is a set of program statements, all of which are mutually inter-dependent. This article reports a large scale empirical study of dependence clusters in C program source code. The study reveals that large dependence clusters are surprisingly commonplace. Most …
Despite the extensiveness of recent investigations on static typing for XML, parametric polymorphism has rarely been treated. This well-established typing discipline can also be useful in XML processing in particular for programs involving “parametric schemas,” that is, schemas p…
This article describes an approach to program optimization based on transformations, where temporal logic is used to specify side conditions, and strategies are created which expand the repertoire of transformations and provide a suitable level of abstraction. We demonstrate the …
This article explains how to construct a ranking function for any program that is proved terminating by size-change analysis . The “principle of size-change termination” for a first-order functional language with well-ordered data is intuitive: A program terminates on all inputs,…
This article describes a method for transforming any given set of Datalog rules into an efficient specialized implementation with guaranteed worst-case time and space complexities, and for computing the complexities from the rules. The running time is optimal in the sense that on…
In the design phase of software development, the designer must make many fundamental design decisions concerning the architecture of the system. Incorrect decisions are relatively easy and inexpensive to fix if caught during the design process, but the difficulty and cost rise si…
Interoperability is big business, a fact to which .NET, the JVM, and COM can attest. Language designers are well aware of this, and they are designing programming languages that reflect it—for instance, SML.NET, F#, Mondrian, and Scala all treat interoperability as a central desi…
Predicate dispatch is an object-oriented (OO) language mechanism for determining the method implementation to be invoked upon a message send. With predicate dispatch, each method implementation includes a predicate guard specifying the conditions under which the method should be …