1,205 papers · page 16 of 61
Peter Sewell, Pawel T. Wojciechowski, Asis Unyapoth
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…
Fausto Spoto, Fred Mesnard, Étienne Payet
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 …
Vivy Suhendra, Abhik Roychoudhury, Tulika Mitra
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…
Peter H. Welch, Jan Bækgaard Pedersen
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…
Eran Yahav, Mooly Sagiv
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…
Xiaotong Zhuang, Santosh Pande
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…
Umut A. Acar, Guy E. Blelloch, Matthias Blume, Robert Harper, Kanat Tangwongsan
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…
Zena M. Ariola, Aaron Bohannon, Amr Sabry
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…
Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk
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…
Massimo Bartoletti, Pierpaolo Degano, Gian-Luigi Ferrari, Roberto Zunino
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…
Giuseppe Castagna, Nils Gesbert, Luca Padovani
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…
Shlomi Dolev, Yinnon A. Haviv, Mooly Sagiv
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…
Mark Harman, David W. Binkley, Keith B. Gallagher, Nicolas Gold, Jens Krinke
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 …
Haruo Hosoya, Alain Frisch, Giuseppe Castagna
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…
Sara Kalvala, Richard Warburton, David Lacey
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 …
Chin Soon Lee
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,…
Yanhong A. Liu, Scott D. Stoller
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…
Steve MacDonald, Kai Tan, Jonathan Schaeffer, Duane Szafron
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…
Jacob Matthews, Robert Bruce Findler
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…
Todd D. Millstein, Christopher Frost, Jason Ryder, Alessandro Warth
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 …