1,205 papers · page 17 of 61
Joseph M. Morris, Alexander Bunkenburg, Malcolm Tyrrell
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…
Ana Lúcia de Moura, Roberto Ierusalimschy
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…
Peter W. O'Hearn, Hongseok Yang, John C. Reynolds
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…
Keshav Pingali, Kathryn S. McKinley
No abstract available.
Davide Sangiorgi
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…
Christian Schulte, Peter J. Stuckey
No abstract available.
Jon Sneyers, Tom Schrijvers, Bart Demoen
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 …
Efe Yardimci, Michael Franz
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 …
Yutao Zhong, Xipeng Shen, Chen Ding
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…
Manuel Arenaz, Juan Touriño, Ramon Doallo
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…
Amir M. Ben-Amram
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…
Cinzia Bernardeschi, Nicoletta De Francesco, Giuseppe Lettieri, Luca Martini, Paolo Masci
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…
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
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 …
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse
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…
Sapan Bhatia, Charles Consel, Calton Pu
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…
James Cheney, Christian Urban
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…
Daniel E. Cooke, J. Nelson Rushton, Brad Nemanich, Robert G. Watson, Per Andersen
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…
Daniel S. Dantas, David Walker, Geoffrey Washburn, Stephanie Weirich
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…
Roland Ducournau
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…
Cormac Flanagan, Stephen N. Freund, Marina Lifshin, Shaz Qadeer
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…