We present a novel approach to optimize incremental scope-bounded checking of programs using a relational constraint solver. Given a program and its correctness specification, scope-bounded checking encodes control-flow and data-flow of bounded code segments into declarative formulas and uses constraint solvers to search for correctness violations. For non-trivial programs, the formulas are often complex and represent a heavy workload that can choke the solvers. To scale scope-bounded checking, our previous work introduced an incremental approach that uses the program's control-flow as a basis of partitioning the program and generating several sub-formulas, which represent simpler problem instances for the underlying solvers. This paper introduces a new approach that uses the program's dataflow, specifically variable-definitions, as a basis for incremental checking. Experimental results show that the use of data-flow provides a significant reduction in the number of variables in the encoded formulas over the previous control-flow-based approach, thereby further improving scalability of scopebounded checking.

Parallel changes are becoming increasingly prevalent in the development of large scale software system. To further study the relationship between parallel changes and faults, we have designed and implemented a semantic conflict analyzer (SCA) to detect semantic interference between parallel changes. SCA combines data dependency analysis and program slicing. Data dependency analysis can disclose the semantic structure of the program. And program slicing can identify which semantic structures are impacted by a change. By comparing the overlap between impacts of two changes, SCA can detect if there are semantic interference between the two changes. An experiment with an industrial project shows that SCA can detect a significant portion of the faults in highly parallel changes. SCA is effective in predicting faults (based on "direct" semantic interference detection) in changes made within a short time period. SCA is both efficient (averaging less than two minutes) and scalable (requiring only the local context)

Parallel developments are becoming increasingly prevalent in the building and evolution of large-scale software systems. Our previous studies of a large industrial project showed that there was a linear correlation between the degree of parallelism and the likelihood of defects in the changes. To further study the relationship between parallel changes and faults, we have designed and implemented an algorithm to detect "direct" semantic interference between parallel changes. To evaluate the analyzer's effectiveness in fault prediction, we designed an experiment in the context of an industrial project. We first mine the change and version management repositories to find sample versions sets of different degrees of parallelism. We investigate the interference between the versions with our analyzer. We then mine the change and version repositories to find out what faults were discovered subsequent to the analyzed interfering versions. We use the match rate between semantic interference and faults to evaluate the effectiveness of the analyzer in predicting faults. Our contributions in this evaluative empirical study are twofold. First, we evaluate the semantic interference analyzer and show that it is effective in predicting faults (based on "direct" semantic interference detection) in changes made within a short time period. Second, the design of our experiment is itself a significant contribution and exemplifies how to mine software repositories rather than use artificial cases for rigorous experimental evaluations.

The publish/subscribe paradigm provides a loosely coupled form of interaction that is well suitable for the large-scale distributed systems. In this paper, we introduce the semantic Web technologies into the publish/subscribe systems and propose a new type of publish/subscribe system. In the system, concept models are represented as ontologies, events are represented as RDF graphs, and subscriptions are represented as RDF graph patterns. The system can match events with subscriptions based on the semantics of events, and support events with complex data structures such as graphs