|
PLDog submit an article | search | rss feed | register | feedback | about |
| Registration | |
| You need to register to submit articles and post comments. Read this to find out how. |
| view next 12 articles | view previous 12 articles |
| Korat: automated testing based on Java predicates | |||
|
|||
| This paper presents Korat, a novel framework for automated testing of Java programs. Given a formal specification for a method, Korat uses the method precondition to automatically generate all (nonisomorphic) test cases up to a given small size. Korat then executes the method on each test case, and uses the method postcondition as a test oracle to check the correctness of each output.To generate test cases for a method, Korat constructs a Java predicate (i.e., a method that returns a boolean) from the method's pre-condition. The heart of Korat is a technique for automatic test case generation: given a predicate and a bound on the size of its inputs, Korat generates all (nonisomorphic) inputs for which the predicate returns true. Korat exhaustively explores the bounded input space of the predicate but does so efficiently by monitoring the predicate's executions and pruning large portions of the search space.This paper illustrates the use of Korat for testing several data structures, including some from the Java Collections Framework. The experimental results show that it is feasible to generate test cases from Java predicates, even when the search space for inputs is very large. This paper also compares Korat with a testing framework based on declarative specifications. Contrary to our initial expectation, the experiments show that Korat generates test cases much faster than the declarative framework. | |||
| Chandrasekhar Boyapati, Sarfraz Khurshid, and Darko Marinov | |||
|
|||
| Refinement-Based Context-Sensitive Points-To Analysis for Java | |||
|
|||
| We present a scalable and precise context-sensitive points-to analysis with three key properties: (1) filtering out of unrealizable paths, (2) a context-sensitive heap abstraction, and (3) a context-sensitive call graph. Previous work [21] has shown that all three properties are important for precisely analyzing large programs, e.g., to show safety of downcasts. Existing analyses typically give up one or more of the properties for scalability. We have developed a refinement-based analysis that succeeds by simultaneously refining handling of method calls and heap accesses, allowing the analysis to precisely analyze important code while entirely skipping irrelevant code. The analysis is demand-driven and client-driven, facilitating refinement specific to each queried variable and increasing scalability. In our experimental evaluation, our analysis proved the safety of 61% more casts than one of the most precise existing analyses across a suite of large benchmarks. The analysis checked the casts in under 13 minutes per benchmark (taking less than 1 second per query) and required only 35MB of memory, far less than previous approaches. | |||
| Manu Sridharan, Ras Bodik | |||
| Appears in PLDI 2006 | |||
| bodik says: [ You must be logged in to view this comment. ] | |||
|
|||
| Automatic Generation of Multi-path Vulnerability Signatures | |||
|
|||
| dawnsong says: [ You must be logged in to view this comment. ] | |||
|
|||
| Towards Automatic Discovery of Deviations in Binary Implementations with Applications to Error Detection and Fingerprint Generation | |||
|
|||
| dawnsong says: [ You must be logged in to view this comment. ] | |||
|
|||
| Effective Static Race Detection for Java | |||
|
|||
| We present a novel technique for static race detection in Java programs, comprised of a series of stages that employ a combination of static analyses to successively reduce the pairs of memory accesses potentially involved in a race. We have implemented our technique and applied it to a suite of multi-threaded Java programs. Our experiments show that it is precise, scalable, and useful, reporting tens to hundreds of serious and previously unknown concurrency bugs in large, widely-used programs with few false alarms. |
|||
| Mayur Naik, Alex Aiken, John Whaley | |||
| Appears in PLDI 2006 | |||
| bodik says: [ You must be logged in to view this comment. ] | |||
|
|||
| Concurrency Analysis for Parallel Programs with Textually Aligned Barriers | |||
|
|||
| Amir Kamil and Katherine Yelick | |||
| Appears in LCPC 2005 | |||
| yelick says: [ You must be logged in to view this comment. ] | |||
|
|||
| Hierarchical Pointer Analysis for Distributed Programs | |||
|
|||
| Amir Kamil and Katherine Yelick | |||
| Appears in SAS 2007 | |||
|
|||
| Optimization and Performance Modeling of Stencil Computations on Modern Microprocessors | |||
|
|||
| Stencil-based kernels constitute the core of many important scientific applications on block-structured grids. Unfortunately, these codes achieve a low fraction of peak performance, due primarily to the disparity between processor and main memory speeds. In this paper, we explore the impact of trends in memory subsystems on a variety of stencil optimization techniques and develop performance models to analytically guide our optimizations. Our work targets cache reuse methodologies across single and multiple stencil sweeps, examining cache-aware algorithms as well as cache-oblivious techniques on the Intel Itanium2, AMD Opteron, and IBM Power5. Additionally, we consider stencil computations on the heterogeneous multi-core design of the Cell processor, a machine with an explicitly-managed memory hierarchy. Overall our work represents one of the most extensive analyses of stencil optimizations and performance modeling to date. Results demonstrate that recent trends in memory system organization have reduced the efficacy of traditional cache- blocking optimizations. We also show that a cache-aware implementation is significantly faster than a cache-oblivious approach, while the explicitly managed memory on Cell enables the highest overall efficiency: Cell attains 88% of algorithmic peak while the best competing cache-based processor only achieves 54% of algorithmic peak performance. |
|||
| Kaushik Datta, Shoaib Kamil, Samuel Williams, Leonid Oliker, John Shalf, Katherine Yelick | |||
|
|||
| Optimization of Sparse Matrix-Vector Multiplication | |||
|
|||
| Samuel Williams, Leonid Oliker, Richard Vuduc, John Shalf, Katherine Yelick, James Demmel | |||
| Appears in Supercomputing 2007 | |||
|
|||
| CS294: Brief project descriptions | |||
|
|||
| Post your brief project description as a comment to this article. One posting per team. |
|||
|
|||
| Project idea related to SMT solvers | |||
|
|||
| Log in to get the PDF description of the proposed project and an initial solution approach. | |||
| sseshia says: [ You must be logged in to view this comment. ] | |||
|
|||
| Towards Automatic Generation of Vulnerability Signatures | |||
|
|||
| dawnsong says: [ You must be logged in to view this comment. ] | |||
|
|||
| view next 12 articles | view previous 12 articles |