| Protocols for Asymetric Communication Channels |
DEC 97 |
25 pages |
| Authors:
Micah Adler; Bruce M. Maggs; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
 | This paper examines the problem of communicating an n-bit data item from a client to a server, where the data is drawn from a distribution D that is known to the server but not to the client. Since this question is motivated by asymmetric communication channels, our primary goal is to limit the number of bits transmitted by the client. We present several protocols in which the expected number of ... |
|
| Architectural Implications of a Family of Irregular Applications |
14 NOV 1997 |
23 pages |
| Authors:
David O'Hallaron; Jonathan R. Shewchuk; Thomas Gross; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Irregular applications based on sparse matrices are at the core of many important scientific computations. Since the importance of such applications is likely to increase in the future, high-performance parallel and distributed systems must provide adequate support for such applications. We characterize a family of irregular scientific applications and derive the demands they will place on the communication systems of future parallel systems. Running time of these applications is dominated ... |
|
| Experiments in Spoken Document Retrieval at CMU |
NOV 1997 |
14 pages |
| Authors:
M. A. Siegler; M. J. Witbrock; S. T. Slattery; K. Seymore; R. E. Jones; A. G. Hauptmann; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We describe our submission to the TREC-6 Spoken Document Retrieval "SDR" track and the speech recognition and the information retrieval engines. We present SDR evaluation results and a brief analysis. A few developments and experiments are also described in detail including: Vocabulary size experiments, which assess the effect of words missing from the speech recognition vocabulary. For our 51,000-word vocabulary the effect was minimal. Speech recognition using a stemmed language ... |
|
| A Tracker for Broken and Closely-Spaced Lines |
OCT 1997 |
18 pages |
| Authors:
Naoki Chiba; Takeo Kanade; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We propose an automatic line tracking method which can deal with broken or closely-spaced line segments more accurately than previous methods over an image sequence. The method uses both grey scale information of the original images and geometric attributes of line segments. By using our hierarchical optical flow technique, we can get a good prediction of line segments in a consecutive frame even with large motion. The line attribute of ... |
|
| Lattice Based Language Models |
SEP 1997 |
29 pages |
| Authors:
Pierre Dupont; Ronald Rosenfeld; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This paper introduces lattice based language models, a new language modeling paradigm. These models construct multi-dimensional hierarchies of partitions and select the most promising partitions to generate the estimated distributions. We discussed a specific two dimensional lattice and propose two primary features to measure the usefulness of each node: the training-set history count and the smoothed entropy of its prediction. Smoothing techniques are reviewed and a generalization of the conventional ... |
|
| A Hierarchical Fair Service Curve Algorithm for Link-Sharing, Real-Time and Priority Services |
SEP 1997 |
62 pages |
| Authors:
Ion Stoica; Hui Zhang; T. S. Ng; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| In this paper, we study hierarchical resource management models and algorithms that support both link-sharing and guaranteed real-time services with decoupled delay (priority) and bandwidth allocation. We extend the service curve based QoS model, which defines both delay and bandwidth requirements of a class, to include fairness, which is important for the integration of real-time and hierarchical link-sharing services. The resulting Fair Service Curve link- sharing model formalizes the goals ... |
|
| Well-Spaced Points for Numerical Methods |
AUG 1997 |
173 pages |
| Authors:
Dafna Talmor; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| A numerical method for the solution of a partial differential equation (PDE) requires the following steps: (1) discretizing the domain (mesh generation); (2) using an approximation method and the mesh to transform the problem into a linear system; (3) solving the linear system. The approximation error and convergence of the numerical method depend on the geometric quality of the mesh, which in turn depends on the size and shape of ... |
|
| The Options Approach to Software Prototyping Decisions |
JUL 97 |
23 pages |
| Authors:
Prasad Chalasani; Somesh Jha; Kevin Sullivan; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Abstract Prototyping is often used to predict, or reduce the uncertainty over, the future profitability of a software design choice. Boehm 1 pioneered the use of techniques from statistical decision theory to provide a basis for making prototyping decisions. However his approach does not apply to situations where the software engineer has the flexibility of waiting for more information before making a prototyping decision. Also, his framework considers only uncertainty ... |
|
| The Fox Project: Advanced Development of Systems Software |
JUN 97 |
6 pages |
| Authors:
CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The long-term objectives of the Carnegie Mellon Fox Project are to improve the design and construction of systems software and to further the development of advanced programming language technology. We use principles and techniques from the mathematical foundations of programming languages, including semantics, type theory, and logic, to design and implement systems software, including operating systems, network protocols, and distributed systems. Much of the implementation work is conducted in the ... |
|
| Delaunay Refinement Mesh Generation |
18 MAY 1997 |
214 pages |
| Authors:
Jonathan R. Shewchuk; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Delaunay refinement is a technique for generating unstructured meshes of triangles or tetrahedral suitable for use in the finite element method or other numerical methods for solving partial differential equations. Popularized by the engineering community in the mid-1980s, Delaunay refinement operates by maintaining a Delaunay triangulation or Delaunay tetrahedralization, which is refined by the insertion of additional vertices. The placement of these vertices is chosen to enforce boundary conformity and ... |
|
| Survey of Polygonal Surface Simplification Algorithms |
01 MAY 1997 |
32 pages |
| Authors:
Paul S. Heckbert; Michael Garland; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This paper surveys methods for simplifying and approximating polygonal surfaces. A polygonal surface is a piecewise-linear surface in 3-D defined by a set of polygons; typically a set of triangles. Methods from computer graphics, computer vision, cartography, computational geometry, and other fields are classified, summarized, and compared both practically and theoretically. The surface types range from height fields (bivariate functions), to manifolds, to non-manifold self-intersecting surfaces. Piecewise-linear curve simplification is ... |
|
| A Formal Approach to Software Architecture |
MAY 97 |
248 pages |
| Authors:
Robert J. Allen; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| As software systems become more complex, the overall system structure-or software architecture-becomes a central design problem. A system's architecture provides a model of the system that suppresses implementation detail, allowing the architect to concentrate on the analyses and decisions that are most crucial to structuring the system to satisfy its requirements. Unfortunately, current representations of software architecture are informal and ad hoc. While architectural concepts are often embodied in infrastructure ... |
|
| Vocal Tract Length Normalization for Large Vocabulary Continuous Speech Recognition |
MAY 97 |
|
| Authors:
Puming Zhan; Alex Waibel; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
 | Generally speaking, the speaker-dependence of a speech recognition system stems from speaker-dependent speech feature. The variation of vocal tract length and/or shape is one of the major source of inter-speaker variations. In this paper, we address several methods of vocal tract length normalization (VTLN) for large vocabulary continuous speech recognition: (1) explore the bilinear warping VTLN in frequency domain; (2) propose a speaker-specific Bark/ Mel scale VTLN in Bark/Mel domain; ... |
|
| Verification of Floating-Point Adders |
APR 1997 |
22 pages |
| Authors:
Yirng-An Chen; Randal E. Bryant; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The floating-point division bug in Intel's Pentium processor and the overflow flag erratum of the FIST instruction in Intel's Pentium Pro and Pentium II processor have demonstrated the importance and the difficulty of verifying floating-point arithmetic circuits. In this paper, we present a "black box" version of verification of FP adders. In our approach, FP adders are verified by an extended word-level SMV using reusable specifications without knowing the circuit ... |
|
| Video Skimming and Characterization through the Combination of Image and Language Understanding Techniques |
03 FEB 97 |
14 pages |
| Authors:
Michael A. Smith; Takeo Kanade; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Digital video is rapidly becoming important for education, entertainment, and a host of multimedia applications. With the size of the video collections growing to thousands of hours, technology is needed to effectively browse segments in a short time without losing the content of the video. We propose a method to extract the significant audio and video information and create a "skim" video which represents a very short synopsis of the ... |
|
| Level Spacings for SL(2,p) |
15 JAN 97 |
16 pages |
| Authors:
John D. Lafferty; Daniel N. Rockmore; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We investigate the eigenvalue spacing distributions for randomly generated 4-regular Cayley graphs on SL2(Fp) by numerically calculating their spectra. We present strong evidence that the distributions are Poisson and hence do not follow the Gaussian orthogonal ensemble. Among the Cayley graphs of SL2(Fp) we consider are the new expander graphs recently discovered by Y. Shalom. In addition, we use a Markov chain method to generate random 4-regular graphs and observe ... |
|
| Name-It: Association of Face and Name in Video |
20 DEC 96 |
19 pages |
| Authors:
Shin ichi Satoh; Takeo Kanade; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This paper proposes a novel approach to extract meaningful content information from video by collaborative integration of image understanding and natural language processing. As an actual example, we developed a system that associates faces and names in videos, called Name-It, which is given news videos as a knowledge source, then automatically extracts face and name association as content information. The system can infer the name of a given unknown face ... |
|
| Automatic Modeling and Localization for Object Recognition |
25 OCT 1996 |
143 pages |
| Authors:
Mark D. Wheeler; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Being able to accurately estimate an object's pose (location) in an image is important for practical implementations and applications of object recognition. Recognition algorithms often trade off accuracy of the pose estimate for efficiency -- usually resulting in brittle and inaccurate recognition. One solution is object localization -- a local search for the object's true pose given a rough initial estimate of the pose. Localization is made difficult by the ... |
|
| Model Checking Algorithms for the mu-Calculus |
23 SEP 96 |
28 pages |
| Authors:
Sergey Berezin; Edmund Clarke; Somesh Jha; Will Marrero; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The propositional mu-calculus is a powerful language for expressing properties of transition systems by using least and greatest fixpoint operators. Recently, the mu-calculus has generated much interest among researchers in computer-aided verification. This interest stems from the fact that many temporal and program logics can be encoded into the mu-calculus. In addition, important relations between transition systems, such as weak and strong bisimulation equivalence, also have fixpoint characterizations. Wide-spread use ... |
|
| Java as an Intermediate Language |
12 AUG 96 |
19 pages |
| Authors:
Jonathan C. Hardwick; Jay Sipelstein; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We present our experiences in using Java as an intermediate language for the high level programming language NESL. First, we describe the design and implementation of a system for translating VOODE the current intermediate language used by NESL-into Java. Second, we evaluate this translation by comparing the performance of the original VOODE implementation with several variants of the Java implementation. The translator was easy to build, and the generated Java ... |
|
| Fast Algorithms for Finding O(Congestion + Dilation) Packet Routing Schedules |
JUL 96 |
16 pages |
| Authors:
F. T. Leighton; Bruce M. Maggs; Andrea W. Richa; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| In 1988, Leighton, Maggs, and Rao showed that for any network and any set of packets whose paths through the network are fixed and edge-simple, there exists a schedule for routing the packets to their destinations in O(c + d) steps using constant-size queues, where C is the congestion of the paths in the network, and d is the length of the longest path. The proof, however, used the Lova'sz ... |
|
| Understanding Customer Dissatisfaction with Underutilized Distributed File Servers |
JUL 1996 |
20 pages |
| Authors:
Erik Riedel; Garth Gibson; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Modern distributed file systems very successfully cache file data on client machines. While this ensures that average response time is low, it also ensures large variance in response time because operations that must contact remote servers are much slower. Direct measurement of these remote servers show that their overall utilization can be quite low, 3% in our data, while users are simultaneously sufficiently dissatisfied with performance to pay for a ... |
|
| Design of the Programming Language Forsythe |
28 JUN 96 |
71 pages |
| Authors:
John C. Reynolds; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This is a description of the programming language Forsythe, which is a descendant of Algol 60 intended to be as uniform and general as possible, while retaining the basic character of its progenitor. |
|
| Symbolic Techniques for Formally Verifying Industrial Systems |
18 JUN 96 |
23 pages |
| Authors:
Sergio Campos; Edmund M. Clarke; Marius Minea; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The design of correct computer systems is extremely difficult. However, it is also a very important task. Such systems are frequently used in applications where failures can have catastrophic consequences, or cause significant financial losses. Simulation and testing are the most widely used verification techniques, but they can only show the presence of errors and cannot demonstrate correctness. Until lately formal methods were too expensive to be used in industrial ... |
|
| Focus of Attention in Video Conferencing |
JUN 96 |
29 pages |
| Authors:
Jie Yang; Leejay Wu; Alex Waibel; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| In this report we present an approach to low bitrate video teleconferencing by focusing attention on important information. We show that by selectively degrading the quality of less important regions, more important regions can be sent without loss of quality but with greatly reduced bandwidth requirements. Low bitrate transmission for real-time video delivery over a dynamic network is achieved by region blurring and cropping. A prototype system has been developed ... |
|
| Fundamental Challenges in Mobile Computing |
FEB 96 |
|
| Authors:
Mahadev Satyanarayanan; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This paper is an answer to the question: 'What is unique and conceptually different about mobile computing?' The paper begins by describing a set of constraints intrinsic to mobile computing, and examining the impact of these constraints on the design of distributed systems. Next, it summarizes the key results of the Coda and Odyssey systems. Finally, it describes the research opportunities in five important topics relevant to mobile computing: caching ... |
|
| Research in Appearance Description for Machine Vision |
31 JAN 96 |
30 pages |
| Authors:
Steve Shafer; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The key barrier to application of machine vision in unconstrained environments is the complexity of image formation in the world and the resultant difficulty of characterizing it concisely. If we could create a general yet concise description of image formation, we would have a vocabulary for discussing the complexity of specific scenes and the assumptions of specific machine vision approaches. In this research, the investigators are attempting to develop such ... |
|
| Cryptographic Postage Indicia |
JAN 96 |
15 pages |
| Authors:
J. D. Tygar; Bennet Yee; Nevin Heintze; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We apply cryptographic techniques to the problem of fraud in metered mail. We describe a mail system that combines off-the-shelf barcode technology, tamper-proof devices, and cryptography in a fully-integrated secure franking system. This system provides protection against: (1) Tampering with postage meters to fraudulently obtain extra postage; (2) Forging and copying of stamps; (3) Unauthorized use of postage meters; and (4) Stolen postage meters. We provide detailed justification for our ... |
|
| Mobile Information Access |
JAN 1996 |
16 pages |
| Authors:
M. Satyanarayanan; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The ability to access information on demand when mobile will be a critical capability in the 21st century. In this paper, we examine the fundamental forces at work in mobile computing systems and explain how they constrain the problem of mobile information access. From these constraints, we derive the importance of adaptivity as a crucial requirement of mobile clients. We then develop a taxonomy of adaptation strategies, and summarize our ... |
|
| Safe Kernel Extensions Without Run-Time Checking |
96 |
16 pages |
| Authors:
George C. Necula; Peter Lee; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This paper describes a mechanism by which an operating system kernel can determine with certainty that it is safe to execute a binary supplied by an untrusted source. The kernel first defines a safety policy and makes it public. Then, using this policy, an application can provide binaries in a special form called proof-carrying code, or simply PCC. Each PCC binary contains, in addition to the native code, a formal ... |
|
| A Computational Meta Logic for the Horn Fragment of LF |
06 DEC 95 |
158 pages |
| Authors:
Carsten Schuermann; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The logical framework LF is a type theory defined by Harper, Honsell and Plotkin. It is well-suited to serve as'a meta language to represent deductive systems. LF and its logic programming implementation Elf are also well-suited to represent meta-theoretic proofs and their computational content, but search for such proofs lies outside the framework. This thesis proposes a computational meta logic (MLF) for the Horn fragment of LF. The Horn fragment ... |
|
| Just Draw It! Programming by Sketching Storyboards |
27 NOV 95 |
18 pages |
| Authors:
James A. Landay; Brad A. Myers; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Current interactive user interface construction tools make it hard for a user interface designer to illustrate the behavior of an interface. These tools focus on specifying widgets and making it easy to manipulate details such as colors, alignment, and fonts. They can show what the interface will look like, but make it hard to show what it will do, since they require programming or scripting in order to specify all ... |
|
| Tracking Human Faces in Real-Time |
NOV 95 |
34 pages |
| Authors:
Jie Yang; Alex Waibel; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Many applications in human computer interaction (HCI) require tracking a human face. In this report, we address two important issues for tracking human faces in real-time: what to track and how to track. We present a stochastic model to characterize skin-colors of human faces. The information provided by the model is sufficient for tracking a human face in a various poses and views. The model can be adapted in real ... |
|
| NESL: A Nested Data-Parallel Language. (Version 3.1) |
19 SEP 95 |
65 pages |
| Authors:
Guy E. Blelloch; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This report describes NESL, a strongly-typed, applicative, data- parallel language. NESL is intended to be used as a portable interface for programming a variety of parallel and vector computers, and as a basis for teaching parallel algorithms. Parallelism is supplied through a simple set of data-parallel constructs based on sequences, including a mechanism for applying any function over the elements of a sequence in parallel and a rich set of ... |
|
| Smart Cards in Hostile Environments |
14 SEP 95 |
7 pages |
| Authors:
Howard Gobioff; Sean Smith; J. D. Tygar; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| One often hears the claim that smart cards are the solution to a number of security problems, including those arising in point-of-sale systems. This paper argues that many proposed smart card systems still lack effective security for point-of-sale applications. We consider the point-of-sale terminal as a potentially hostile environment to the smart card. Moreover, we discuss several types of modifications that can be made to smart cards to improve their ... |
|
| The Harmonic Sieve: A Novel Application of Fourier Analysis to Machine Learning Theory and Practice |
23 AUG 95 |
148 pages |
| Authors:
Jeffrey C. Jackson; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This thesis presents new positive results--both theoretical and empirical--in machine learning. The primary learning-theoretic contribution is the Harmonic Sieve, the first efficient algorithm for learning the well-studied class of Disjunctive Normal Form (DNF) expressions (learning is accomplished within the Probably Approximately Correct model with respect to the uniform distribution using membership queries). Of particular interest is the novel use of Fourier methods within the algorithm. Specifically, all prior Fourier-based learning ... |
|
| Exploiting Structured Data in Wide-Area Information Systems |
AUG 95 |
14 pages |
| Authors:
John Ockerbloom; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Information produced by outside parties, such as ill the World Wide Web, is increasingly important in many software applications. Effective use of this information requires the ability to exploit its semantic structure. Unfortunately, existing wide-area information systems force data to be distributed in either a lowest-common-denominator form, or in a form meaningful only to programs designed around a particular application. The former results in significant loss of information, while the ... |
|
| Natural Negotiation for Believable Agents |
JUN 95 |
24 pages |
| Authors:
W. S. Reilly; Joseph Bates; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Believable agents will often need to engage in social behaviors with other agents and with a user. Believable social behaviors need to meet a number of requirements: they must be robust, they must reflect and affect the emotional state of the agent, they must take into account the interpersonal relationships with the other behavior participants, and, most importantly, they must show off the artistically defined personality of the agent. We ... |
|
| The Acquisition and Utilization of Spatial and Functional Knowledge for Imagery Analysis |
31 MAY 95 |
30 pages |
| Authors:
David M. McKeown Jr.; Abraham Walker; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
|
| Informed Prefetching and Caching |
11 MAY 95 |
26 pages |
| Authors:
R. H. Patterson; Garth A. Gibson; Eka Ginting; Daniel Stodolsky; Jim Zelenka; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The underutilization of disk parallelism and file cache buffers by traditional file systems induces I/O stall time that degrades the performance of modern microprocessor-based systems. In this paper, we present aggressive mechanisms that tailor file system resource management to the needs of I/O- intensive applications. In particular, we show how to use application-disclosed access patterns (hints) to expose and exploit I/O parallelism and to allocate dynamically file buffers among three ... |
|
| An Efficient Technique for Tracking Nondeterministic Execution and its Applications |
MAY 95 |
20 pages |
| Authors:
E. N. Elnozahy; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This report describes a technique for using instruction counters to track non determinism in the execution of operating system kernels and user programs. The operating system records the number of instructions between consecutive nondeterministic events and information about their nature during normal operation. During an analysis phase, the execution is repeated under the control of a monitor, and the nondeterministic events are applied at the same instructions as during the ... |
|
| Word Level Symbolic Model Checking: A New Approach for Verifying Arithmetic Circuits |
MAY 95 |
22 pages |
| Authors:
E. Clarke; X. Zhao; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The highly-publicized division error in the Pentium has emphasized the importance of formal verification of arithmetic operations. Symbolic model checking techniques based on binary decision diagrams (BDDs) have been successful in verifying control logic. However, lack of proper representation for functions that map boolean vectors into integers has prevented this technique from being used for verifying arithmetic circuits. We have used hybrid decision diagrams to represent the integer functions that ... |
|
| Efficient Parallel Algorithms for Planar DAGs |
MAY 95 |
65 pages |
| Authors:
Stephen Guattery; Gary L. Miller; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We show that testing reachability in a planar DAG can be performed in parallel in O(log n log* n) time (0 (log n) time using randomization) using 0(n) processors. In general we give a paradigm for reducing a planar DAG to a constant size and then expanding it back. This paradigm is developed from a property of planar directed graphs we refer to as the Poincare' index formula. Using this ... |
|
| Application of Convex Sampling to Optimization and Contingency Table Generation/Counting |
MAY 95 |
111 pages |
| Authors:
John Mount; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The optimization problem of minimizing a linear objective function over a general convex body given only by a weak membership oracle is a central problem in convex optimization. Traditional methods require the (expensive) construction of separating relations (cuts) or gradient information (which is often expensive). We demonstrate how a sampling procedure can be used as the central routine in a randomized polynomial time algorithm for approximately minimizing a linear objective ... |
|
| Dome: Parallel Programming in a Heterogeneous Multi-User Environment |
APR 95 |
27 pages |
| Authors:
Jose N. Arabe; Adam Beguelin; Bruce Lowekamp; Erik Seligman; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Writing parallel programs for distributed multi-user computing environments is a difficult task. The Distributed object migration environment (Dome) addresses three major issues of parallel computing in an architecture independent manner: ease of programming, dynamic load balancing, and fault tolerance. Some programmers, with modest effort, can write parallel programs that are automatically distributed over a heterogeneous network, dynamically load balanced as the program runs, and able to survive compute node and ... |
|
| Hybrid Decision Diagrams. Overcoming the Limitations of MTBDDs and BMDs |
APR 95 |
20 pages |
| Authors:
B. Clarke; M. Fujita; X. Zhao; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Functions that map boolean vectors into the integers are important for the design and verification of arithmetic circuits. MTBDDs and BMDs have been proposed for representing this class of functions. We discuss the relationship between these methods and describe a generalization called hybrid decision diagrams which is often much more concise. We show how to implement arithemetic operations efficiently for hybrid decision diagrams. In practice, this is one of the ... |
|
| Using Dynamic Sets to Speed Search in World Wide Information Systems |
27 MAR 95 |
18 pages |
| Authors:
David C. Steere; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Search on wide area distributed systems is plagued by the high latencies inherent in remote access. A solution is to prefetch information before it is requested by the searcher to hide latency. But this raises the problem of knowing what to prefetch, since fetching data that will not be used can actually hurt performance. This paper proposes extending the Unix file model to support dynamic sets, short-lived and unordered collections ... |
|
| Model Checking Software Systems: A Case Study |
10 MAR 95 |
26 pages |
| Authors:
Jeannette M. Wing; Mandana Vaziri-Farahani; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Model checking is a proven successful technology for verifying hardware. It works, however, on only fInite state machines, and most software systems have infInitely many states. Our approach to applying model checking to software hinges on identifying appropriate abstractions that exploit the nature of both the system, S, and the property, phi to be verifIed. We check phi on an abstracted, but fInite, model of S. Following this approach we ... |
|
| Human-Computer Interaction (HCI) Specialization Track Masters of Software Engineering (MSE) Program. Revision |
01 MAR 95 |
13 pages |
| Authors:
Carol L. Hoover; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| There is an increasing demand for software to implement human- computer interfaces. Software engineers who develop these interfaces need an understanding of the interactions between the human, the available computer technology, and human tasks. They should also understand empirical methods used to evaluate the usability of existing human-computer interfaces. The Human- Computer Interaction Specialization Track, which is an option within the Masters of Software Engineering (MSE) Program at Carnegie Mellon ... |
|
| Automatic Tools for Developing Fine-Grained Signal Processing Programs on Multicomputers |
01 MAR 95 |
20 pages |
| Authors:
David R. O'Hallaron; H. T. Kung; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| During the course of this contract we developed the first system that integrates task and data parallelism in a uniform compiler framework. The compiler which is called Fx, translates a dialect of High Performance Fortran into parallel code that runs on distributed memory computer systems such as the Intel Paragon, the Lintel iWarp, the IBM SP/2, and networks of workstations. We demonstrated the effectiveness of our technIque on a wide ... |
|
Reports by Corporate Author
