Binary Translation Using Peephole Superoptimizers (2009)
We present a new scheme for performing binary translation that produces code comparable to or better than existing binary translators with much less engineering effort. Instead of hand-coding the...
Alert Detection in System Logs (2009)
Adam J. Oliner, Alex Aiken, Jon Stearley
We present Nodeinfo, an unsupervised algorithm for anomaly detection in system logs. We demonstrate Nodeinfo’s effectiveness on data from four of the world’s most powerful supercomputers: using...
Binary Translation Using Peephole Superoptimizers (2009)
We present a new scheme for performing binary translation that produces code comparable to or better than existing binary translators with much less engineering effort. Instead of hand-coding the...
Verifying the Safety of User Pointer Dereferences (2009)
Operating systems divide virtual memory addresses into kernel space and user space. The interface of a modern operating system consists of a set of system call procedures that may take pointer...
A Tuning Framework for Software-Managed Memory Hierarchies (2009)
Manman Ren, Alex Aiken, Ji Young Park, William J. Dally, Mike Houston
Achieving good performance on a modern machine with a multi-level memory hierarchy, and in particular on a machine with software-managed memories, requires precise tuning of programs to the...
Sound, Complete and Scalable Path-Sensitive Analysis ∗ (2009)
Isil Dillig, Thomas Dillig, Alex Aiken
We present a new, precise technique for fully path- and contextsensitive program analysis. Our technique exploits two observations: First, using quantified, recursive formulas, path- and...
Flow-Insensitive Type Qualifiers 1 (2009)
Jeffrey S. Foster, Robert Johnson, John Kodumal, Alex Aiken
We describe flow-insensitive type qualifiers, a lightweight, practical mechanism for specifying and checking properties not captured by traditional type systems. We present a framework for adding...
Abstract Sequoia: Programming the Memory Hierarchy (2008)
Kayvon Fatahalian, Timothy J. Knight, Mike Houston, Mattan Erez, Daniel Reiter, Horn Larkhoon, ...
We present Sequoia, a programming language designed to facilitate the development of memory hierarchy aware parallel programs that remain portable across modern machines featuring different memory...
5 Titanium Group (Past and Present) (2008)
Dan Bonachea, Susan Graham, Katherine Yelick, Paul Hilfinger, Alex Aiken, Greg Balls, ...
• Many modeling problems in astrophysics, biology, material science, and other areas require – Enormous range of spatial and temporal scales • To solve interesting problems, one needs: –...
SATURN: A Scalable Framework for Error Detection Using Boolean Satisfiability (2008)
This article presents SATURN, a general framework for building precise and scalable static error detection systems. SATURN exploits recent advances in Boolean satisfiability (SAT) solvers and is path...
ABSTRACT Static Detection of Security Vulnerabilities (2008)
In Scripting Languages, Yichen Xie, Alex Aiken
We present a static analysis algorithm for detecting security vulnerabilities in PHP, a popular server-side scripting language for building web applications. Our analysis employs a novel three-tier...
A Portable Runtime Interface For Multi-Level Memory Hierarchies (2008)
Mike Houston, Ji-young Park, Manman Ren, Timothy Knight, Kayvon Fatahalian, Alex Aiken, ...
We present a platform independent runtime interface for moving data and computation through parallel machines with multi-level memory hierarchies. We show that this interface can be used as a...
Verifying Finite-State Safety Properties on Millions of Lines of Code (2008)
Abstract. We present a context-sensitive, flow-sensitive, field-sensitive, and intraprocedurally path-sensitive static analysis capable of verifying finite-state safety properties of very large...
Alice X. Zheng, Ben Liblit, Michael I. Jordan, Alex Aiken
We present a novel strategy for automatically debugging programs given sampled data from thousands of actual user runs. Our goal is to pinpoint those features that are most correlated with crashes....
We present a new approach to the old problem of adding global mutable state to purely functional languages. Our idea is to extend the language with “witnesses, ” which is based on an arguably...
Abstract Flow-Sensitive Type Qualifiers ∗ (2008)
Jeffrey S. Foster, Tachio Terauchi, Alex Aiken
We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct....
We present an overview of the Saturn program analysis system, including a rationale for three major design decisions: the use of function-at-a-time, or summary-based, analysis, the use of...
Jeffrey S. Foster, Tachio Terauchi, Alex Aiken
We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct....
Abstract Sequoia: Programming the Memory Hierarchy (2008)
Kayvon Fatahalian, Timothy J. Knight, Mike Houston, Mattan Erez, Daniel Reiter, Horn Larkhoon, ...
We present Sequoia, a programming language designed to facilitate the development of memory hierarchy aware parallel programs that remain portable across modern machines featuring different memory...
Flow-Insensitive Type Qualifiers 1 (2008)
Jeffrey S. Foster, Robert Johnson, John Kodumal, Alex Aiken
We describe flow-insensitive type qualifiers, a lightweight, practical mechanism for specifying and checking properties not captured by traditional type systems. We present a framework for adding...
ABSTRACT Bug Isolation via Remote Program Sampling ∗ (2008)
Ben Liblit, Alice X. Zheng, Alex Aiken, Michael I. Jordan
We propose a low-overhead sampling infrastructure for gathering information from the executions experienced by a program’s user community. Several example applications illustrate ways to use...
Saturn: A Scalable Framework for Error Detection using Boolean Satisfiability (2008)
This article presents Saturn, a general framework for building precise and scalable static error detection systems. Saturn exploits recent advances in boolean satisfiability (SAT) solvers and is path...
Automatic Generation of Peephole Superoptimizers (2008)
Abstract Peephole optimizers are typically constructed using human-writtenpattern matching rules, an approach that requires expertise and time, as well as being less than systematic at exploiting all...
Jeffrey S. Foster, Tachio Terauchi, Alex Aiken
We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct....
Alice X. Zheng, Alex Aiken, Michael I. Jordan
Abstract As part of our work on Cooperative Bug Isolation (CBI)we have undertaken to instrument and distribute binaries for a number of large open source projects. This public de-ployment is an...
ABSTRACT Bug Isolation via Remote Program Sampling ∗ (2008)
Ben Liblit, Alice X. Zheng, Alex Aiken, Michael I. Jordan
We propose a low-overhead sampling infrastructure for gathering information from the executions experienced by a program’s user community. Several example applications illustrate ways to use...
ABSTRACT Flow-Sensitive Type Qualifiers (2008)
Jeffrey S. Foster, Tachio Terauchi, Alex Aiken
Categories and Subject Descriptors
Jeffrey S. Foster, Tachio Terauchi, Alex Aiken
We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct....
Notes on Program Analysis (2007)
interpretation provides a suitable basis for justifying the correctness of program analyses. There are two problems, however. The first problem is mostly an annoyance: abstract interpretations are...
liblit @ cs. berkeley. edu (2007)
Katherine Yelick, Alex Aiken, Ben Liblit, Ben Liblit
yelick @ cs. berkeley. edu
Flow-Sensitive Type Qualiers (2007)
Jerey S. Foster, Tachio Terauchi, Alex Aiken, Alex Aiken
We present a system for extending standard type systems with ow-sensitive type qualiers. Users annotate their programs with type qualiers, and inference checks that the annotations are correct. In...
Flow-Sensitive Type Qualiers (2007)
Jerey S. Foster, Tachio Terauchi, Alex Aiken
We present a system for extending standard type systems with ow-sensitive type qualiers. Users annotate their programs with type qualiers, and inference checks that the annotations are correct. In...
Statistical Debugging in the Presence of Multiple Errors (2007)
Ben Liblit Mayur, Ben Liblit, Mayur Naik, Alice X. Zheng, Alex Aiken, Michael I. Jordan
We present a statistical debugging algorithm that operates on very sparsely sampled data drawn from large numbers of user runs. By identifying program behaviors that significantly increase the...
Compilation for explicitly managed memory hierarchies (2007)
Timothy J. Knight, Ji Young, Park Manman, Ren Mike Houston, Mattan Erez, Kayvon Fatahalian, ...
We present a compiler for machines with an explicitly managed memory hierarchy and suggest that a primary role of any compiler for such architectures is to manipulate and schedule a hierarchy of bulk...
Conditional must not aliasing for static race detection (2007)
Abstract Race detection algorithms for multi-threaded programs using thecommon lock-based synchronization idiom must correlate locks with the memory locations they guard. The heart of a proof ofrace...
A capability calculus for concurrency and determinism (2006)
Abstract. We present a capability calculus for checking partial confluence of channel-communicating concurrent processes. Our approach automatically detects more programs to be partially confluent...
3.1 The Locking Property.......................... 14 (2006)
Alex Aiken, Suhabe Bugrara, Isil Dillig, Thomas Dillig, Brian Hackett, Peter Hawkins
Statistical debugging: simultaneous identification of multiple bugs (2006)
Alice X. Zheng, Ben Liblit, Mayur Naik, Alex Aiken
We describe a statistical approach to software debugging in the presence of multiple bugs. Due to sparse sampling issues and complex interaction between program predicates, many generic off-the-shelf...
Effective static race detection for Java (2006)
Mayur Naik, Alex Aiken, John Whaley
Abstract We present a novel technique for static race detection in Java pro-grams, comprised of a series of stages that employ a combination of static analyses to successively reduce the pairs of...
A capability calculus for concurrency and determinism (2006)
A difficulty with writing correct concurrent programs is non-determinism. This paper presents an static system for checking determinism (technically, partial confluence) of communicating concurrent...
A capability calculus for concurrency and determinism (2006)
Abstract. We present a capability calculus for checking partial confluence of channel-communicating concurrent processes. Our approach automatically detects more programs to be partially confluent...
Scalable statistical bug isolation (2005)
Ben Liblit, Alex Aiken, Mayur Naik, Alice X. Zheng
We present a statistical debugging algorithm that isolates bugs in programs containing multiple undiagnosed bugs. Earlier statistical algorithms that focus solely on identifying predictors that...
Secure information flow as a safety problem (2005)
Abstract. The termination insensitive secure information flow problem can be reduced to solving a safety problem via a simple program transformation. Barthe, D’Argenio, and Rezk coined the term...
AND THE COMMITTEE ON GRADUATE STUDIES (2005)
Sriram Sankaranarayanan, Henny B. Sipma, David Dill, Alex Aiken
in my opinion, it is fully adequate
Scalable statistical bug isolation (2005)
Ben Liblit, Alex Aiken, Mayur Naik, Alice X. Zheng
We present a statistical debugging algorithm that isolates bugs in programs containing multiple undiagnosed bugs. Earlier statistical algorithms that focus solely on identifying predictors that...
Scalable statistical bug isolation (2005)
Ben Liblit, Alex Aiken, Mayur Naik, Alice X. Zheng
We present a statistical debugging algorithm that isolates bugs in programs containing multiple undiagnosed bugs. Earlier statistical algorithms that focus solely on identifying predictors that...
Scalable Statistical Bug Isolation (2005)
Ben Liblit Computer, Ben Liblit, Alex Aiken, Mayur Naik, Alice X. Zheng
We present a statistical debugging algorithm that isolates bugs in programs containing multiple undiagnosed bugs. Earlier statistical algorithms that focus solely on identifying predictors that...
Banshee: A scalable constraint-based analysis toolkit (2005)
Abstract. We introduce Banshee, a toolkit for constructing constraintbased analyses. Banshee’s novel features include a code generator for creating customized constraint resolution engines,...
Secure information flow as a safety problem (2005)
Abstract. The termination insensitive secure information flow problem can be reduced to solving a safety problem via a simple program transformation. Barthe, D’Argenio, and Rezk coined the term...
Public deployment of cooperative bug isolation (2004)
Ben Liblit, Mayur Naik, Alice X. Zheng, Alex Aiken, Michael I. Jordan
As part of our work on Cooperative Bug Isolation (CBI) we have undertaken to instrument and distribute binaries for a number of large open source projects. This public deployment is an important step...
Public deployment of cooperative bug isolation (2004)
As part of our work on Cooperative Bug Isolation (CBI) we have undertaken to instrument and distribute binaries for a number of large open source projects. This public deployment is an important step...
Memory Management with Use-Counted Regions (2004)
Tachio Terauchi, Tachio Terauchi, Alex Aiken, Alex Aiken
We introduce a new region-based memory management technique that allows flexible memory usage patterns and is provably safe. Our technique is explicit and manual like C's malloc and free, and it...
Public Deployment of Cooperative Bug Isolation (2004)
As part of our work on Cooperative Bug Isolation (CBI) we have undertaken to instrument and distribute binaries for a number of large open source projects. This public deployment is an important step...
Public deployment of cooperative bug isolation (2004)
As part of our work on Cooperative Bug Isolation (CBI) we have undertaken to instrument and distribute binaries for a number of large open source projects. This public deployment is an important step...
Type systems for distributed data sharing (2003)
Ben Liblit, Alex Aiken, Katherine Yelick
Abstract. Parallel programming languages that let multiple processors access shared data provide a variety of sharing mechanisms and memory models. Understanding a language’s support for data...
Types for Lexically-Scoped Access Control * (2003)
Tachio Terauchi, Alex Aiken, Jeffrey S. Foster, Tachio Terauchi, Jeffrey S. Foster, Alex Aiken
1 Introduction In situations where a program P interacts with one or more untrusted program components U, a well-specifiedaccess control policy protects P 's resources from unwanted operations...
Type systems for distributed data sharing (2003)
Ben Liblit, Alex Aiken, Katherine Yelick
Abstract. Parallel programming languages that let multiple processors access shared data provide a variety of sharing mechanisms and memory models. Understanding a language’s support for data...
Bug isolation via remote program sampling (2003)
Ben Liblit, Alex Aiken, Alice X. Zheng, Michael I. Jordan
We propose a low-overhead sampling infrastructure for gathering information from the executions experienced by a program 's user community. Several example applications illustrate ways to use...
Statistical Debugging of Sampled Programs (2003)
Alice Zheng Ee, Alice X. Zheng, Ben Liblit, Michael I. Jordan, Alex Aiken
We present a novel strategy for automatically debugging programs given sampled data from thousands of actual user runs. Our goal is to pinpoint those features that are most correlated with crashes....
Winnowing: Local Algorithms for Document Fingerprinting (2003)
Saul Schleimer, Daniel S. Wilkerson, Alex Aiken
Digital content is for copying: quotation, revision, plagiarism, and file sharing all create copies. Document fingerprinting is concerned with accurately identifying copying, including small partial...
Bug Isolation via Remote Program Sampling (2003)
Ben Liblit Alex, Alice X. Zheng, Alex Aiken, Michael I. Jordan
We propose a low-overhead sampling infrastructure for gathering information from the executions experienced by a program 's user community. Several example applications illustrate ways to use...
Distributed program sampling (2003)
We propose a sampling infrastructure for gathering information about software from the set of runs experienced by its user community. We show how to gather random samples with very low overhead for...
Checking and Inferring Local Non-Aliasing (2003)
Alex Aiken, John Kodumal, Jeffrey S. Foster, Tachio Terauchi
In prior work [15] we studied a language construct restrict that allows programmers to specify that certain pointers are not aliased to other pointers used within a lexical scope. Among other...
Sampling User Executions for Bug Isolation (2003)
Ben Liblit Alex, Alex Aiken, Alice X. Zheng, Michael I. Jordan
Introduction Many computer scientists think of a program as either correct (i.e. it meets some specification) or incorrect (i.e. it does not meet some specification). But industrial software...
Bug Isolation via Remote Program Sampling (2003)
Ben Liblit Alex, Alice X. Zheng, Alex Aiken, Michael I. Jordan
We propose a low-overhead sampling infrastructure for gathering information from the executions experienced by a program 's user community. Several example applications illustrate ways to use...
Statistical Debugging of Sampled Programs (2003)
Alice Zheng Ee, Alice X. Zheng, Michael I. Jordan, Ben Liblit, Alex Aiken
We present a novel strategy for automatically debugging programs given sampled data from thousands of actual user runs. Our goal is to pinpoint those features that are most correlated with crashes....
Abstract Building a Better Backtrace: Techniques for Postmortem Program Analysis ∗ (2002)
Ben Liblit, Alex Aiken, Ben Liblit
After a program has crashed, it can be difficult to reconstruct why the failure occurred, or what actions led to the error. We propose a family of analysis techniques that use the evidence left...
Flow-Sensitive Type Qualifiers (2002)
Jeffrey S. Foster, Tachio Terauchi, Alex Aiken
We present a system for extending standard type systems with flow-sensitive type qualifiers. Users annotate their programs with type qualifiers, and inference checks that the annotations are correct....
Flow-sensitive type qualifiers (2002)
Jeffrey S. Foster, Robert Johnson, John Kodumal, Alex Aiken
We describe flow-insensitive type qualifiers, a lightweight, practical mechanism for specifying and checking properties not captured by traditional type systems. We present a framework for adding...
Language support for regions (2001)
Region-based memory management systems structure memory by grouping objects in regions under program control. Memory is reclaimed by deleting regions, freeing all objects stored therein. Our compiler...
Language Support and Compilation Techniques for Regions (2000)
Language Support and Compilation Techniques for Regions Region-based memory management systems structures memory by grouping objects in regions under program control. Memory is reclaimed by deleting...
Titanium: A High-Performance Java Dialect (1998)
Kathy Yelick, Luigi Semenzato, Geoff Pike, Carleton Miyamoto, Ben Liblit, Arvind Krishnamurthy, ...
Abstract Titanium is a language and system for high-performance parallel scientific computing. Titaniumuses Java as its base, thereby leveraging the advantages of that language and allowing us to...
Titanium: A High-Performance Java Dialect (1998)
Kathy Yelick, Luigi Semenzato, Geoff Pike, Carleton Miyamoto, Ben Liblit, Arvind Krishnamurthy, ...
Titanium is a language and system for high-performance parallel scientific computing. Titanium uses Java as its base, thereby leveraging the advantages of that language and allowing us to focus...
Titanium: A High-Performance Java Dialect (1998)
Kathy Yelick, Luigi Semenzato, Geoff Pike, Carleton Miyamoto, Ben Liblit, Arvind Krishnamurthy, ...
Titanium is a language and system for high-performance parallel scientific computing. Titanium uses Java as its base, thereby leveraging the advantages of that language and allowing us to focus...
Memory Management with Explicit Regions (1998)
Much research has been devoted to studies of and algorithms for memory management based on garbage collection or explicit allocation and deallocation. An alternative approach, region-based memory...
Titanium: A High-Performance Java Dialect (1998)
Kathy Yelick Luigi, Luigi Semenzato, Geoff Pike, Carleton Miyamoto, Ben Liblit, Arvind Krishnamurthy, ...
Titanium is a language and system for high-performance parallel scientific computing. Titanium uses Java as its base, thereby leveraging the advantages of that language and allowing us to focus...
Titanium: A High-Performance Java Dialect (1998)
Kathy Yelick, Luigi Semenzato, Geoff Pike, Carleton Miyamoto, Ben Liblit, Arvind Krishnamurthy, ...
Titanium is a language and system for high-performance parallel scientific computing. Titanium uses Java as its base, thereby leveraging the advantages of that language and allowing us to focus...