2,199 papers · page 71 of 110
The Ambient Calculus is a process calculus where processes may reside within a hierarchy of locations and modify it. The purpose of the calculus is to study mobility, which is seen as the change of spatial configurations over time. In order to describe properties of mobile comput…
Design patterns have earned a place in the developer's arsenal of tools and techniques for software development. They have proved so useful, in fact, that some have called for their promotion to programming language features. In turn this has rekindled the age-old debate over the…
Set-based analysis of logic programs provides an accurate method for descriptive type-checking of logic programs. The key idea of this method is to upper approximate the least model of the program by a regular set of trees. In 1991, Frühwirth, Shapiro, Vardi and Yardeni raised th…
Mark and sweep garbage collectors are known for using time proportional to the heap size when sweeping memory, since all objects in the heap, regardless of whether they are live or not, must be visited in order to reclaim the memory occupied by dead objects. This paper introduces…
We propose an automatic method to enforce trace properties on programs. The programmer specifies the property separately from the program; a program transformer takes the program and the property and automatically produces another “equivalent” pogram satisfying the property. This…
We study the abstract interpretation of temporal calculi and logics in a general syntax, semantics and abstraction independent setting. This is applied to the @@@@-calculus, a generalization of the μ-calculus with new reversal and abstraction modalities as well as a new time-symm…
Various code certification systems allow the certification and static verification of important safety properties such as memory and control-flow safety. These systems are valuable tools for verifying that untrusted and potentially malicious code is safe before execution. However…
This paper is a contribution to the already existing series of work on the algorithmic principles of interprocedural analysis. We consider the generalization to the case of parallel programs. We give algorithms that compute the sets of backward resp. forward reachable configurati…
We introduce a language for creating and manipulating certificates, that is, digitally signed data based on public key cryptography, and a system for revoking certificates. Our approach provides a uniform mechanism for secure distribution of public key bindings, authorizations, a…
We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis.…
In this paper we describe the syntax, semantics, and implementation of the constraint logic programming language CLP(F) and we prove that the implementation is sound. A CLP(F) constraint is a conjunction of equations and inequations in a first order theory of analytic univariate …
This paper describes a new approach to generic functional programming, which allows us to define functions generically for all datatypes expressible in Haskell. A generic function is one that is defined by induction on the structure of types. Typical examples include pretty print…
Java source code is strongly typed, but the translation from Java source to bytecode omits much of the type information originally contained within methods. Type elaboration is a technique for reconstructing strongly typed programs from incompletely typed bytecode by inferring ty…
Procedure extraction is an important program transformation that can be used to make programs easier to understand and maintain, to facilitate code reuse, and to convert “monolithic” code to modular or object-oriented code. Procedure extraction involves the following steps:
Two forms of interferences are individuated in Cardelli and Gordon's Mobile Ambients (MA): plain interferences, which are similar to the interferences one finds in CCS and φ-calculus; and grave interferences, which are more dangerous and may be regarded as programming errors. To …
This paper introduces a language feature, called implicit parameters, that provides dynamically scoped variables within a statically-typed Hindley-Milner framework. Implicit parameters are lexically distinct from regular identifiers, and are bound by a special with construct whos…
Distributed-memory programs are often written using a global address space: any process can name any memory location on any processor. Some languages completely hide the distinction between local and remote memory, simplifying the programming model at some performance cost. Other…
This paper attempts to address the question of why certain dataflow analysis problems can be solved efficiently, but not others. We focus on flow-sensitive analyses, and give a simple and general result that shows that analyses that require the use of relational attributes for pr…
The ambient calculus is a calculus of computation that allows active processes to move between sites. We present an analysis inspired by state-of-the-art pointer analyses that safety and accurately predicts which processes may turn up at what sites during the execution of a compo…
In this article, we add a third dimension to partial redundancy elimination by considering code size as a further optimization goal in addition to the more classical consideration of computation costs and register pressure. This results in a family of sparse code motion algorithm…