Test input generation is one of the key applications of symbolic execution (SE). However, being a path-sensitive technique, SE often faces path explosion even when creating a branch-adequate test suite. Path-merging symbolic execution (PM-SE) alleviates the path explosion problem by summarizing regions of code into disjunctive constraints, thus traversing at once a set of paths with the same prefixes. Previous work has shown that PM-SE can reduce run-time up to 38%, though these improvements can be impaired if the summarized code results in complex constraints or introduces additional symbols that increase the number of branching points in the later execution.Considering these trade-offs, examining the ability of PM-SE to generate branch-adequate test inputs is an open research problem. This paper investigates it by developing a technique that extracts structural coverage-related queries from disjoint constraints. Using this approach, we extend PM-SE to generate branch-adequate test inputs.Experiments compare the effectiveness and efficiency of test input generation by SE and PM-SE techniques. Results show that those techniques are complementary. For some programs, PM-SE yields faster coverage, with fewer generated tests, while for others, SE performs better. In addition, each technique covers branches that the other fails to discover.

We present a web-based Program Analysis Collaboratory (PAClab) tool that helps researchers to obtain realistic program benchmarks using user-defined selection criteria. Based on selection criteria, PAClab identifies relevant projects and its programs from open-source repositories, obtains those programs, and if necessary performs sound program transformations to adapt them to the targeted verification tool. PAClab makes the resulting program benchmarks available for download. PAClab is designed as a scalable, modular, and parametrizable tool that takes advantage of a computer cluster to handle multiple user requests.

As our society has become more information oriented, each individual is expressed, defined, and impacted by information and information technology. While valuable, the current state-of-the-art mostly are designed to protect the enterprise/ organizational privacy requirements and leave the main actor, i.e., the user, un-involved or with the limited ability to have control over his/her information sharing practices. In order to overcome these limitations, algorithms and tools that provide a user-centric privacy management system to individuals with different privacy concerns are required to take into the consideration the dynamic nature of privacy policies which are constantly changing based on the information sharing context and environmental variables. This paper extends the concept of contextual integrity to provide mathematical models and algorithms that enables the creations and management of privacy norms for individual users. The extension includes the augmentation of environmental variables, i.e. time, date, etc. as part of the privacy norms, while introducing an abstraction and a partial relation over information attributes. Further, a formal verification technique is proposed to ensure privacy norms are enforced for each information sharing action.

As an important extension of symbolic execution (SE), probabilistic symbolic execution (PSE) computes execution probabilities of program paths. Using this information, PSE can prioritize path exploration strategies. To calculate the probability of a path PSE relies on solution counting approaches for the path constraint. The correctness of a solution counting approach depends on the methodology used to count solutions and whether a path constraint maintains a one-to-one relation with program input values. This work focuses on the latter aspect of the solution counting correctness for string constraints. In general, maintaining a one-to-one relation is not always possible, especially in the presence of non-linear constraints. To deal with this issue, researchers that work on PSE for numerical domains either analyze programs with linear constraints, or develop novel techniques to handle solution counting of non-linear constraints. For the string domain, however, previous work on PSE mainly focuses on efficient and accurate solution counting for automata-based string models and has not investigated whether a one-to-one relationship between the strings encoded by automata and input string values is preserved. In this work we demonstrate that traditional automata-based string models fail to maintain one-to-one relations and propose to use the weighted automata model, which preserves the one-to-one relation between the path constraint it encodes and the input string values. We use this model to implement a string constraint solver and show its correctness on a set of non-trivial synthetic benchmarks. We also present an empirical evaluation of traditional and proposed automata solvers on real-world string constraints. The evaluations show that while being less efficient than traditional automata models, the weighted automata model maintains correct solution counts.

Novel research ideas require strong evaluations. Modern software engineering research evaluation typically requires a set of benchmark programs. Open source software repositories have provided a great opportunity for researchers to find such programs for use in their evaluations. Many tools/techniques have been developed to help automate the curation of open source software. There has also been encouragement for researchers to provide their research artifacts so that other researchers can easily reproduce the results. We argue that these two trends (i.e., curating open source software for research evaluation and the providing of research artifacts) drive the need for Software Engineer Collaboratories (SEClabs). We envision research communities coming together to create SEClab instances, where research artifacts can be made publicly available to other researchers. The community can then vet such artifacts and make them available as a service, thus turning the collaboratory into a Collaboratory as a Service (CaaS). If our vision is realized, the speed and transparency of research will drastically increase.

A key challenge in implementing an efficient and precise data flow analysis is determining how to abstract the domain of values that a program variable can take on and how to update abstracted values to reflect program semantics. Such updates are performed by a transfer function and recent work by Thakur, Elder and Reps defined the bilateral algorithm for computing the most precise transfer function for a given abstract domain. In this paper, we identify and exploit the special case where abstract domains are comprised of disjoint subsets. For such domains, transfer functions computed using a customized algorithm can improve performance and in combination with symbolic modeling of block-level transfer functions improve precision as well. We implemented these algorithms in Soot and used them to perform data flow analysis on more than 100 non-trivial Java methods drawn from open source projects. Our experimental data are promising as they demonstrate that a 25-fold reduction in analysis time can be achieved and precision can be increased relative to existing methods.

The precision and scalability of path-sensitive program analyses depend on their ability to distinguish feasible and infeasible program paths. Analyses express path feasibility as the satisfiability of conjoined branch conditions, which is then decided by cooperating decision procedures such as those in satisfiability modulo theory (SMT) solvers. Consequently, efficient underlying decision procedures are key to precise, scalable program analyses. When we investigate the branch conditions accumulated by inter-procedural path-sensitive analyses of object-oriented programs, we find that many relate to an object's dynamic type. These conditions arise from explicit type tests and the branching implicit in dynamic dispatch and type casting. These conditions share a common form that comprises a fragment of the theory of partial orders, which we refer to as type-based partial orders (TPO) . State-of-the-art SMT solvers can heuristically instantiate the quantified formulae that axiomatize partial orders, and thereby support TPO constraints. We present two custom decision procedures with significantly better performance. On benchmarks that reflect inter-procedural path-sensitive analyses applied to significant Java systems, the custom procedures run three orders of magnitude faster. The performance of the two decision procedures varies across benchmarks, which suggests that a portfolio approach may be beneficial for solving constraints generated by program analyses.

Symbolic execution tools query constraint solvers for tasks such as determining the feasibility of program paths. Therefore, the effectiveness of such tools depends on their constraint solvers.

Coverage measures help to determine whether a test suite exercises a program adequately according to a testing criterion. Many existing measures, however, are defined over coverage domains that cannot be precisely calculated, rendering them of limited value in assessing the extent of testing activities. To exploit the use of such measures, we formalize saturation-based test adequacy, a form of adequacy focused on the rate at which coverage increases during test suite execution. We define a family of coverage metrics for concurrent program testing that are well-suited to saturation-based adequacy and present a study that explores their cost and effectiveness. The results of this study suggest that saturation-based testing can serve as an effective complement to traditional notions of coverage-based testing.