1,205 papers · page 17 of 61
We present a new approach to adding state and state-changing commands to a term language. As a formal semantics it can be seen as a generalization of predicate transformer semantics, but beyond that it brings additional opportunities for specifying and verifying programs. It is b…
This article advocates the revival of coroutines as a convenient general control abstraction. After proposing a new classification of coroutines, we introduce the concept of full asymmetric coroutines and provide a precise definition for it through an operational semantics. We th…
We investigate proof rules for information hiding, using the formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a logical connective gives rise to a f…
No abstract available.
The origins of bisimulation and bisimilarity are examined, in the three fields where they have been independently discovered: Computer Science, Philosophical Logic (precisely, Modal Logic), Set Theory. Bisimulation and bisimilarity are coinductive notions, and as such are intimat…
No abstract available.
Constraint Handling Rules (CHR) is a high-level rule-based programming language which is increasingly used for general-purpose programming. We introduce the CHR machine, a model of computation based on the operational semantics of CHR. Its computational power and time complexity …
We have built a runtime compilation system that takes unmodified sequential binaries and improves their performance on off-the-shelf multiprocessors using dynamic vectorization and loop-level parallelization techniques. Our system, Azure, is purely software based and requires no …
On modern computer systems, the memory performance of an application depends on its locality. For a single execution, locality-correlated measures like average miss rate or working-set size have long been analyzed using reuse distance —the number of distinct locations accessed be…
The recognition of program constructs that are frequently used by software developers is a powerful mechanism for optimizing and parallelizing compilers to improve the performance of the object code. The development of techniques for automatic recognition of computational kernels…
This article considers an algorithmic problem related to the termination analysis of programs. More specifically, we are given bounds on differences in sizes of data values before and after every transition in the program's control-flow graph. Our goal is to infer program termina…
Bytecode verification is a key point in the security chain of the Java platform. This feature is only optional in many embedded devices since the memory requirements of the verification process are too high. In this article we propose an approach that significantly reduces the us…
WS-SecurityPolicy is a declarative language for configuring web services security mechanisms. We describe a formal semantics for WS-SecurityPolicy and propose a more abstract language for specifying secure links between web services and their clients. We present the architecture …
We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic implementations of cryptographic algorithms. The concrete implementation is for production and interoperability testing. The symbo…
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 allows the reuse of previously impleme…
Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, α-equivalence). This article investigates logic programming based on nominal logic. We des…
SequenceL is a concise, high-level language with a simple semantics that provides for the automatic derivation of many iterative and parallel control structures. The semantics repeatedly applies a “Normalize-Transpose-Distribute” operation to functions and operators until base ca…
This article defines AspectML, a typed functional, aspect-oriented programming language. The main contribution of AspectML is the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, AspectML allows program…
Subtype tests are an important issue in the implementation of object-oriented programming languages. Many techniques have been proposed, but none of them perfectly fulfills the five requirements that we have identified: constant-time, linear-space, multiple inheritance, dynamic l…
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. Atomic methods are amenable to sequ…