1,205 papers · page 33 of 61
SLG resolution uses tabling to evaluate nonfloundering normal logic pr ograms according to the well-founded semantics. The SLG-WAM, which forms the engine of the XSB system, can compute in-memory recursive queries anorder of magnitute fasterthan current deductive databases. At th…
In this article, we present a new framework for elimination-based exhaustive and incremental data flow analysis using the DJ graph representation of a program.Unlike previous approaches to elimination-based incremental data flow analysis, our approach can handle arbitrary structu…
Region Inference is a program analysis which infers lifetimes of values. It is targeted at a runtime model in which the store consists of a stack of regions and memory management predominantly consists of pushing and popping regions, rather than performing garbage collection. Reg…
Previously published algorithms for LR ( k ) incremental parsing are inefficient, unnecessarily restrictive, and in some cases incorrect. We present a simple algorithm based on parsing LR( k ) sentential forms that can incrementally parse an arbitrary number of textual and/or str…
This article describes a general-purpose program analysis that computes global control-flow and data-flow information for higher-order, call-by-value languages. The analysis employs a novel form of polyvariance called polymorhic splitting that uses let-expressions as syntactic cl…
In this article we investigate the trade-off between time and space efficiency in scheduling and executing parallel irregular computations on distributed-memory machines. We employ acyclic task dependence graphs to model irregular parallelism with mixed granularity, and we use di…
We outline the design and detail the implementation of a language extension for abstracting types and for decoupling subtyping and inheritance in C++. This extension gives the user more of the flexibility of dynamic typing while retaining the efficiency and security of static typ…
PIM is an equational logic designed to function as a “transformational toolkit” for compilers and other programming tools that analyze and manipulate imperative languages. It has been applied to such problems as program slicing, symbolic evaluation, conditional constant propagati…
We introduce a simple compositional proof system for proving (partial) correctness of concurrent constraint programs (CCP). The proof system is based on a denotational approximation of the strongest postcondition semantics of CCP programs. The proof system is proved to be correct…
A formal refinement calculus targeted at system-level descriptions in the IEEE standard hardware description language VHDL is described here. Refinement can be used to develop hardware description code that is “correct by construction”. the calculus is closely related to a Hoare-…
Correctly predicting the direction that branches will take is increasingly important in today's wide-issue computer architectures. The name program-based branch prediction is given to static branch prediction techniques that base their prediction on a program's structure. In this…
The use of regular expressions for text search is widely known and well understood. It is then surprising that the standard techniques and tools prove to be of limited use for searching structured text formatted with SGML or similar markup languages. Our experience with structure…
This article describes a technique based on network grammars and abstraction to verify families of state-transition systems. The family of state-transition systems is represented by a context-free network grammar. Using the structure of the network grammar our technique construct…
Reduced product of abstract domains is a rather well-known operation for domain composition in abstract interpretation. In this article, we study its inverse operation, introducing a notion of domain complementation in abstract interpretation. Complementation provides as systemat…
The advent of ever more complex reactive systems in increasingly critical areas calls for the development of automated verification techniques.Model checking is one such technique, which has proven quite successful.However, the state-explosion problem remains a major stumbling bl…
Knowledge of low-level control flow is essential for many compiler optimizations. In systems with tail-call optimization, the determination of interprocedural control flow is complicated by the fact that because of tail-call optimization, control flow at procedure returns is not …
The high cost and growing importance of interprocedural data flow analysis have led to an increased interest in demand-driven algorithms. In this article, we present a general framework for developing demand-driven interprocedural data flow analyzers and report our experience in …
One useful technique for combating the state explosion problem is to exploit symmetry when performing temporal logic model checking. In previous work it is shown how, using some basic notions of group theory, symmetry may be exploited for the full range of correctness properties …
In this article we present a compiler-based technique to help develop correct real-time systems. The domain we consider is that of multiprogrammed real-time applications, in which periodic tasks control physical systems via interacting with external sensors and actuators. While a…
Recognizing and transforming loops are essential steps in any attempt to improve the running time of a program. Aggressive restructuring techniques have been developed for single-entry (reducible) loops, but restructurers and the dataflow and dependence analysis they rely on ofte…