Programmers often have to spend a significant amount of time inspecting the software code and execution traces to identify the root cause of a software bug. For a multithreaded program, debugging is even more challenging due to the subtle interactions between concurrent threads and the often astronomical number of possible interleavings. In this work, we propose a logical constraint-based symbolic analysis method to aid in the diagnosis of concurrency bugs and find their root causes, which can be later used to recommend repairs. In our method, the diagnosis process is formulated as a set of constraint solving problems. By leveraging the power of constraint satisfiability (SAT) solvers and a bounded model checker, we perform a semantic analysis of the sequential computation as well as the thread interactions. The analysis is ideally suited for handling software with small to medium code size but complex concurrency control, such as device drivers, synchronization protocols, and concurrent data structures. We have implemented our method in a software tool and demonstrated its effectiveness in diagnosing subtle concurrency bugs in multithreaded C programs. / Master of Science

This dissertation advances the state-of-the-art in information retrieval (IR) based automatic bug localization for large software systems. We present techniques from three generations of IR based bug localization and compare their performances on our large and diverse bug localization dataset --- the Bugzbook dataset. The three generations span over fifteen years of research in mining software repositories for bug localization and include: (1) the generation of simple bag-of-words (BoW) based techniques, (2) the generation in which software-centric information such as bug and code change histories as well as structured information embedded in bug reports and code files are exploited to improve retrieval, and (3) the third and most recent generation in which order and semantic relationships between terms are modeled to improve the performance of bug localization systems. The dissertation also presents a novel technique called SCOR (Source Code Retrieval with Semantics and Order) which combines Markov Random Fields (MRF) based term-term ordering dependencies with semantic word vectors obtained from neural network based word embedding algorithms, such as word2vec, to better localize bugs in code files. The results presented in this dissertation show that while term-term ordering and semantic relationships significantly improve the performance when they are modeled separately in retrieval systems, the best precisions in retrieval are obtained when they are modeled together in a single retrieval system. We also show that the semantic representations of software terms learned by training the word embedding algorithm on a corpus of software repositories can be used to perform search in new software code repositories not present in the training corpus of the word embedding algorithm.<br>

Hardware verification currently takes more than 50% of the whole verification time. There is a sustained effort to improve the efficiency of the verification process, which in the past helped deliver a large variety of supporting tools. The past years though did not see any major technology change that would bring the improvements that the process really needs (H. Foster 2013) (Wilson Research Group 2012). The existing approach to verification does not provide that type of qualitative jump anymore. This work is introducing a new tactic, providing a modern alternative to the existing approach to the verification problem. The novel approach I use in this research has the potential of significantly improve the process, way beyond incremental changes. It starts with acknowledging the huge amounts of data that follows the hardware development process from inception to the final product and in considering the data not as a quantitative by-product but as a qualitative supply of information on which we can develop a smarter verification. The approach is based on data already generated throughout the process currently used by verification engineers to zoom into the details of different verification aspects. By using existing machine learning approaches we can zoom out and use the same data to extract information, to gain knowledge that we can use to guide the verification process. This approach allows an apparent lack of accuracy introduced by data discovery, to achieve the overall goal. The latest advancements in machine learning and data mining offer a base of a new understanding and usage of the data that is being passed through the process. This work takes several practical problems for which the classical verification process reached a roadblock, and shows how the new approach can provide a jump in productivity and efficiency of the verification process. It focuses on four different aspects of verification to prove the power of this new approach: reducing effort redundancy, guiding verification to areas that need it first, decreasing time to diagnose, and designing tests for coverage efficiency. / text