Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. MDESL is a Verilog-like language, which is a multithreaded discrete event simulation language. It contains interesting features such as event-driven computation and shared-variable concurrency. This paper considers how the algebraic semantics links with the operational semantics for MDESL. Our approach is from both the theoretical and practical aspects. The link is proceeded by deriving the operational semantics from the algebraic semantics. Firstly, we present the algebraic semantics for MDESL. We introduce the concept of head normal form. Secondly we present the strategy of deriving operational semantics from algebraic semantics. We also investigate the soundness and completeness of the derived operational semantics with respect to the derivation strategy. Our theoretical approach is complemented by a practical one, we use the theorem proof assistant Coq to formalize the algebraic laws and the derived operational semantics. Meanwhile, the soundness and completeness of the derived operational semantics is also verified via the mechanical approach in Coq. Our approach is a novel way to formalize and verify the correctness and equivalence of different semantics for MDESL in both a theoretical approach and a practical approach.

Family-based-analysis strategies have recently shown very promising potentials for improving efficiency in applying quality-assurance techniques to variant-rich programs, as compared to variant-by-variant approaches. These strategies require a single program representation superimposing all program variants in a syntactically well-formed, semantically sound and variant-preserving manner, which is usually not available and manually hard to obtain in practice. We present a novel methodology, called SiMPOSE, for automatically generating superimpositions of existing program variants to facilitate family-based analyses of variant-rich software. Our N-way model-merging methodology integrates control-flow automaton (CFA) representations of N variants of a C program into one unified CFA representation, constituting a unified program abstraction as used internally by many recent software-analysis tools. To cope with the complexity of N-way merging, we (1) utilize principles of similarity-propagation to reduce the number of N-way matches, and (2) decompose sets of N variants into subsets thus enabling incremental N-way merging. In our experimental evaluation, we apply our SiMPOSE tool to collections of realistic C programs. The results reveal very impressive efficiency improvements of family-based analyses, by an average factor of up to 2.9 for unit-test generation and 2.4 for model-checking, as compared to variant-by-variant practices, thus clearly amortizing the additional effort for N-way merging.

Self-admitted technical debt(SATD) has been proposed to identify debt that is intentionally introduced during software development. Previous studies leveraged human-summarized patterns or text mining techniques to detect SATD in source code comments. However, several characteristics of SATD features in code comments, e.g., vocabulary diversity, project uniqueness, length and semantic variations, pose a big challenge to the accuracy of pattern or text-mining based SATD detection. Furthermore, although text-mining based method outperforms pattern-based method in prediction accuracy, the text features it uses are less intuitive than human-summarized patterns, which makes the prediction results hard to explain. To improve the accuracy of SATD prediction, we propose a Convolutional Neural Network (CNN)-based approach to detect SATD comments. To improve the explainability of our model's prediction results, we exploit the computational structure of CNNs to identify key phrases and patterns in code comments that are most relevant to SATD. We conducted an extensive set of experiments with 62,566 code comments from 10 open-source projects and a user study with 150 comments of another three projects. Our evaluation confirms the effectiveness of different aspects of our approach and its superior performance, generalizability, adaptability and explainability over current state-of-the-art traditional text-mining based methods for SATD classification.