Search

Writing specifications about program behavior is hard. Writing specifications about non-functional effects such as resource usage is often even harder. If manually instrumenting the program is not an option, programmers have to rely on comment-based specification languages like JML to introduce ghost variables and other fairly abstract concepts that are complicated and hard to maintain. Even worse, most static analysis tools nowadays operate on bit- or bytecode and cannot process those type of specifications To address this problem, we propose a library-based specification formalism for time complexity in Java. The approach is inspired by the success of assertion libraries like CodeContracts and Guava. Our library provides a set of methods and enumerated types that allow the user to write complexity assertions in a 'human' readable form and without instrumenting the code. On the backend, we provide a bytecode rewriting tool that uses these assertions to automatically instrument the program with counter variables. The transformed program can then be checked via testing or off-the-shelf automated static analyzers

Producing specifications by dynamic (runtime) analysis of program executions is potentially unsound, because the analyzed executions may not fully characterize all possible executions of the program. In practice, how accurate are the results of a dynamic analysis? This paper describes the results of an investigation into this question, determining how much specifications generalized from program runs must be changed in order to be verified by a static checker. Surprisingly, small test suites captured nearly all program behavior required by a specific type of static checking; the static checker guaranteed that the implementations satisfy the generated specifications, and ensured the absence of runtime exceptions. Measured against this verification task, the generated specifications scored over 90% on precision, a measure of soundness, and on recall, a measure of completeness.This is a positive result for testing, because it suggests that dynamic analyses can capture all semantic information of interest for certain applications. The experimental results demonstrate that a specific technique, dynamic invariant detection, is effective at generating consistent, sufficient specifications for use by a static checker. Finally, the research shows that combining static and dynamic analyses over program specifications has benefits for users of each technique, guaranteeing soundness of the dynamic analysis and lessening the annotation burden for users of the static analysis.

Understanding large software systems is difficult. Traditionally, automated tools are used to assist program understanding. However, the representations constructed by these tools often require prohibitive time and space. Demand-driven techniques can be used to reduce these requirements. However, the use of pointers in modern languages introduces additional problems that do not integrate well with these techniques. We present new techniques for effectively coping with pointers in large software systems written in the C programming language and use our techniques to implement a program slicing tool.First, we use a fast, flow-insensitive, points-to analysis before traditional data-flow analysis. Second, we allow the user to parameterize the points-to analysis so that the resulting program slices more closely match the actual program behavior. Such information cannot easily be obtained by the tool or might otherwise be deemed unsafe. Finally, we present data-flow equations for dealing with pointers to local variables in recursive programs. These equations allow the user to select an arbitrary amount of calling context in order to better trade performance for precision.To validate our techniques, we present empirical results using our program slicer on large programs. The results indicate that cost-effective analysis of large programs with pointers is feasible using our techniques.