Context: As more time has been spent on code comprehension activities during software development, automatic code summarization has received much attention in software engineering research, with the goal of enhancing software comprehensibility. In the meantime, it is prevalently known that a good knowledge about the declaration and the use of method parameters can effectively enhance the understanding of the associated methods. A traditional approach used in software development is to declare the types of method parameters. Objective: In this work, we advocate parameter‐level code summarization and propose a novel approach to automatically generate parameter summaries of a given method. Parameter summarization is considerably challenging, as neither do we know the kind of information of the parameters that can be employed for summarization nor do we know the methods for retrieving such information. Method: We present paramTrans, which is a novel approach for parameter summarization. paramTrans characterizes the semantic features from parameter‐related information based on transformer; it also explores three fusion strategies for absorbing the method‐level information to enhance the performance. Moreover, to retrieve parameter‐related information, a parameter slicing algorithm (named paramSlice) is proposed, which slices the parameter‐related node from the abstract syntax tree (AST) at the statement level. Results: We conducted experiments to verify the effectiveness of our approach. Experimental results show that our approach possesses an effective ability in summarizing parameters; such ability can be further enhanced by understanding the available summaries about individual methods, through the introduction of three fusion strategies. Conclusion: We recommend developers employ our approach as well as the fusion strategies to produce parameter summaries to enhance the comprehensibility of code.

A wide range of verification methods have been proposed to verify the safety properties of deep neural networks ensuring that the networks function correctly in critical applications. However, many well-known verification tools still struggle with complicated network architectures and large network sizes. In this work, we propose a network reduction technique as a pre-processing method prior to verification. The proposed method reduces neural networks via eliminating stable ReLU neurons, and transforming them into a sequential neural network consisting of ReLU and Affine layers which can be handled by most verification tools. We instantiate the reduction technique on the state-of-the-art complete and incomplete verification tools, including$\alpha,\beta$-crown, VeriNet and PRIMA. Our experiments on a large set of benchmarks indicate that the proposed technique can significantly reduce neural networks and speed up existing verification tools. Furthermore, the experiment results also show that network reduction can improve the availability of existing verification tools on many networks by reducing them into sequential neural networks.

Debugging is known to be a notoriously painstaking and time-consuming task. As one major family of automated debugging, statistical debugging approaches have been well investigated over the past decade, which collect failing and passing executions and apply statistical techniques to identify discriminative elements as potential bug causes. Most of the existing approaches instrument the entire program to produce execution profiles for debugging, thus incurring hefty instrumentation and analysis cost. However, as in fact a major part of the program code is error-free, full-scale program instrumentation is wasteful and unnecessary. This article presents a systematic abstraction refinement-based pruning technique for statistical debugging. Our technique only needs to instrument and analyze the code partially. While guided by a mathematically rigorous analysis, our technique is guaranteed to produce the same debugging results as an exhaustive analysis in deterministic settings. With the help of the effective and safe pruning, our technique greatly saves the cost of failure diagnosis without sacrificing any debugging capability. We apply this technique to two different statistical debugging scenarios: in-house and production-run statistical debugging. The comprehensive evaluations validate that our technique can significantly improve the efficiency of statistical debugging in both scenarios, while without jeopardizing the debugging capability.

Deep learning (DL) brings autonomous vehicles (AVs) close to reality. However, the witness of many safety issues has raised a big concern about the reliability of AVs. To solve this problem, much research has been done to test deep learning-driven AVs. Generally, once a test input is produced, a developer needs to manually check its expected output. However, there often exists massive unlabeled test data (e.g., raw context traces in the real world). It is impractical to manually label all test inputs. Despite some works on automatic generation of test oracles, they are either task-specific or constrained to synthetic inputs. In this paper, we present a general and extensible framework,DeepSuite, to mitigate the manual effort of generating test oracles. The intuition behind is that not all test inputs are equally worth labelling. With limited testing budget, it is desirable to label a test suite with high diversity and a reasonable size. Due to the large search space, to optimize such test suites is of great challenge. To address it,DeepSuiteemploys a three-phase optimization method (i.e., selection, crossover, and mutation) to iteratively select representative but non-redundant test suites. Such conflicting profit/cost objectives are attained through a genetic algorithm with a well-defined multi-objective fitness function. In the experiments, we first show that the diversity of tests can be revealed by test criteria. Then, experiments on three widely-used datasets demonstrated the effectiveness ofDeepSuitein generating test suites with competitive testing coverage and 68.42% smaller size, which greatly improves the data collection efficiency of testing DL-driven autonomous vehicles.

SL-COMP aims at bringing together researchers interested on improving the state of the art of the automated deduction methods for Separation Logic (SL). The event took place twice until now and collected more than 1K problems for different fragments of SL. The input format of problems is based on the SMT-LIB format and therefore fully typed; only one new command is added to SMT-LIB’s list, the command for the declaration of the heap’s type. The SMT-LIB theory of SL comes with ten logics, some of them being combinations of SL with linear arithmetics. The competition’s divisions are defined by the logic fragment, the kind of decision problem (satisfiability or entailment) and the presence of quantifiers. Until now, SL-COMP has been run on the StarExec platform, where the benchmark set and the binaries of participant solvers are freely available. The benchmark set is also available with the competition’s documentation on a public repository in GitHub.

Abstract We present a deductive proof system to automatically prove separation logic entailments by mathematical induction. Our technique is called the mutual induction proof . It is an instance of the well-founded induction, a.k.a., Noetherian induction. More specifically, we propose a novel induction principle based on a well-founded relation of separation logic models. We implement this principle explicitly as inference rules so that it can be easily integrated into a deductive proof system. Our induction principle allows a goal entailment and other entailments derived during the proof search to be used as hypotheses to mutually prove each other. This feature increases the success chance of proving the goal entailment. We have implemented this mutual induction proof technique in a prototype prover and evaluated it on two entailment benchmarks collected from the literature as well as a synthetic benchmark. The experimental results are promising since our prover can prove most of the valid entailments in these benchmarks, and achieves a better performance than other state-of-the-art separation logic provers.

The symbolic-heap fragment of separation logic has been actively developed and advocated for verifying the memory-safety property of computer programs. At present, one of its biggest challenges is to effectively prove entailments containing inductive heap predicates. These entailments are usually proof obligations generated when verifying programs that manipulate complex data structures like linked lists, trees, or graphs. To assist in proving such entailments, this paper introduces a lemma synthesis framework, which automatically discovers lemmas to serve as eureka steps in the proofs. Mathematical induction and template-based constraint solving are two pillars of our framework. To derive the supporting lemmas for a given entailment, the framework firstly identifies possible lemma templates from the entailment's heap structure. It then sets up unknown relations among each template's variables and conducts structural induction proof to generate constraints about these relations. Finally, it solves the constraints to find out actual definitions of the unknown relations, thus discovers the lemmas. We have integrated this framework into a prototype prover and have experimented it on various entailment benchmarks. The experimental results show that our lemma-synthesis-assisted prover can prove many entailments that could not be handled by existing techniques. This new proposal opens up more opportunities to automatically reason with complex inductive heap predicates.

Extract Method is a widely used refactoring operation to improve method comprehension and maintenance. Much research has been done to extract codefragments within the method body to form a new method. Criteria used for identifying extractable code is usually centered around degrees of cohesiveness, coupling and length of the method. However, automatic method extraction techniques have not been highly successful, since it can be hard to concretizethe criteria. In this work, we present a novel system that learns these criteria for Extract Method refactorings from open source repositories. We extractstructural and functional features, which encode the concepts of complexity, cohesion and coupling in our learning model, and train it to extract suitablecode fragments from a given source of a method. Our tool, GEMS, recommends a ranked list of code fragments with high accuracy and greatspeed. We evaluated our approach on several open source repositories and compared it against three state-of-the-art approaches-SEMI, JExtract andJDeodorant. The results on these open-source data show the superiority of our machine-learning-based approach in terms of effectiveness. We develop GEMS asan Eclipse plugin, with the intention to support software reliability through method extraction.

Code clones, being an inevitable by-product of rapid software development, can impact software quality. The introduction of code clone groups and clone genealogies enable software developers to be aware of the presence of and changes to clones as a collective group, they also allow developers to understand how clone groups evolve throughout software life cycle. Due to similarity in codes within a clone group, a change in one piece of the code may require developers to make changes to other clones in the group. Failure in making consistent change to a clone group when necessary is commonly known as "clone consistency-defect", which can adversely impact software reliability. We propose an approach to predict clone consistency-requirement at the time when changes have been made to a clone group. Our predictor is a Bayesian network implemented in WEKA. We build a variant of clone genealogies to collect all consistent/inconsistent changes to clone groups, and extract three sets of attributes from clone groups as input for predicting consistent clone change. These three sets are: code attributes, context attributes and evolution attributes. We conduct experiments on three open source projects. These experiments show that our approach has high precision and recall in predicting clone consistency-requirement. This holistic approach can aid developers in maintaining code clone changes, and avoid potential clone consistency-defect, which can improve the software quality and reliability.

Cooperative statistical debugging is an effective approach for diagnosing production-run failures. To quickly identify failure predictors from the huge program predicate space, existing techniques rely on random or heuristics-guided predicate sampling at the user side. However, none of them can satisfy the requirements of low cost, low diagnosis latency, and high diagnosis quality simultaneously, which are all indispensable for statistical debugging to be practical.

Refactoring is an important way to improve the design of existing code. Identifying refactoring opportunities (i.e., code fragments that can be refactored) in large code bases is a challenging task. In this paper, we propose a novel, automated and scalable technique for identifying cross-function refactoring opportunities that span more than one function (e.g., Extract Method and Inline Method). The key of our technique is the design of efficient vector inlining operations that emulate the effect of method inlining among code fragments, so that the problem of identifying cross-function refactoring can be reduced to the problem of finding similar vectors before and after inlining. We have implemented our technique in a prototype tool named ReDex which encodes Java programs to particular vectors. We have applied the tool to a large code base, 4.5 million lines of code, comprising of 200 bundle projects in the Eclipse ecosystem (e.g., Eclipse JDT, Eclipse PDE, Apache Commons, Hamcrest, etc.). Also, different from many other studies on detecting refactoring, ReDex only searches for code fragments that can be, but have not yet been, refactored in a way similar to some refactoring that happened in the code base. Our results show that ReDex can find 277 cross-function refactoring opportunities in 2 minutes, and 223 cases were labelled as true opportunities by users, and cover many categories of cross-function refactoring operations in classical refactoring books, such as Self Encapsulate Field, Decompose Conditional Expression, Hide Delegate, Preserve Whole Object, etc.

Debugging is known to be a notoriously painstaking and time-consuming task. An essential and yet expensive process in debugging is bug isolation. As one major family of automatic bug isolation, statistical bug isolation approaches have been well studied in the past decade. A recent advancement in this area is the introduction of bug signature that provides contextual information to assist in debugging and several bug signature mining approaches have been reported. All these approaches instrument the entire buggy program to produce profiles for debugging. Consequently, they often incur hefty instrumentation and analysis cost. However, as in fact major part of the program code is error-free, full-scale program instrumentation is wasteful and unnecessary. In this paper, we devise a novel hierarchical instrumentation (HI) technique to perform selective instrumentation so as to enhance the efficiency of statistical debugging. We employ HI technique to predicated bug signature mining (called MPS) recently developed and propose an approach called HIMPS. The empirical study reveals that our technique can achieve around 40% to 60% saving in disk storage usage, time and memory consumption, and performs especially well on large programs. It greatly improves the efficiency of bug signature mining, making a step forward to painless debugging.

Automated techniques have been proposed to either identify refactoring opportunities (i.e., code fragments that can be but have not yet been restructured in a program), or reconstruct historical refactorings (i.e., code restructuring operations that have happened between different versions of a program). In this paper, we propose a new technique that can detect both refactoring opportunities and historical refactorings in large code bases. The key of our technique is the design of vector abstraction and concretization operations that can encode code changes induced by certain refactorings as characteristic vectors. Thus, the problem of identifying refactorings can be reduced to the problem of identifying matching vectors, which can be solved efficiently. We have implemented our technique for Java. The prototype is applied to 200 bundle projects from the Eclipse ecosystem containing 4.5 million lines of code, and reports in total more than 32K instances of 17 types of refactoring opportunities, taking 25 minutes on average for each type. The prototype is also applied to 14 versions of 3 smaller programs (JMeter, Ant, XML-Security), and detects (1) more than 2.8K refactoring opportunities within individual versions with a precision of about 87%, and (2) more than 190 historical refactorings across consecutive versions of the programs with a precision of about 92%.

We propose a pattern-based approach to effectively and efficiently analyzing sequential software engineering (SE) data. Different from other types of SE data, sequential SE data preserves unique temporal properties, which cannot be easily analyzed without much programming effort. In order to facilitate the analysis of sequential SE data, we design a sequential pattern query language (SPQL), which specifies the temporal properties based on regular expressions, and is enhanced with variables and statements to store and manipulate matching states. We also propose a query engine to effectively process the SPQL queries. We have applied our approach to analyze two types of SE data, namely bug report history and source code change history. We experiment with 181,213 Eclipse bug reports and 323,989 code revisions of Android. SPQL enables us to explore interesting temporal properties underneath these sequential data with a few lines of query code and low matching overhead. The analysis results can help better under- stand a software process and identify process violations.

We present an approach to automatically discovering explicit rules for software process evaluation from evaluation histories. Each rule is a conjunction of a subset of attributes in a process execution, characterizing why the execution is normal or anomalous. The discovered rules can be used for stakeholder as expertise to avoid mistakes in the future, thus improving software process quality; it can also be used to compose a classifier to automatically evaluate future process execution. We formulate this problem as a contrasting itemset mining task, and employ the branch-and-bound technique to speed up mining by pruning search space. We have applied the proposed approach to four real industrial projects in a commercial bank. Our empirical studies show that the discovered rules can precisely pinpoint the cause of all anomalous executions, and the classifier built on the rules is able to accurately classify unknown process executions into the normal or anomalous class.

A bug signature is a set of program elements highlighting the cause or effect of a bug, and provides contextual information for debugging. In order to mine a signature for a buggy program, two sets of execution profiles of the program, one capturing the correct execution and the other capturing the faulty, are examined to identify the program elements contrasting faulty from correct. Signatures solely consisting of control flow transitions have been investigated via discriminative sequence and graph mining algorithms. These signatures might be handicapped in cases where the effect of a bug is not manifested by any deviation in control flow transitions. In this paper, we introduce the notion of predicated bug signature\/ that aims to enhance the predictive power of bug signatures by utilizing both data predicates and control-flow information. We introduce a novel ``discriminative itemset generator'' mining technique to generate succinct\/ signatures which do not contain redundant or irrelevant program elements. Our case studies demonstrate that predicated signatures can hint at more scenarios of bugs where traditional control-flow signatures fail.

Distributed systems often contain many behaviorally similar processes, which are conveniently grouped into classes. In system modeling, it is common to specify such systems by describing the class level behavior, instead of object level behavior. While there have been techniques that mine specifications of such distributed systems from their execution traces, these methods only mine object-level specifications involving concrete process objects. This leads to specifications which are large, hard to comprehend, and sensitive to simple changes in the system (such as the number of objects). In this paper, we develop a class level specification mining framework for distributed systems. A specification that describes interaction snippets between various processes in a distributed system forms a natural and intuitive way to document their behavior. Our mining method groups together such interactions between behaviorally similar processes, and presents a mined specification involving “symbolic” Message Sequence Charts. Our experiments indicate that our mined symbolic specifications are significantly smaller than mined concrete specifications, while at the same time achieving better precision and recall.

We propose a tool for inferring transformation specifications from a few examples of original and updated code. These transformation specifications may contain multiple code fragments from within a single function, all of which must be present for the transformation to apply. This makes the inferred transformations context sensitive. Our algorithm is based on depth-first search, with pruning. Because it is applied locally to a collection of functions that contain related changes, it is efficient in practice. We illustrate the approach on an example drawn from recent changes to the Linux kernel.

Specifications are important for many activities during software construction and maintenance process such as testing, verification, debugging and repairing. Despite their importance, specifications are often missing, informal or incomplete because they are difficult to write manually. Many techniques have been proposed to automatically mine specifications describing method call sequence from execution traces or source code using frequent pattern mining. Unfortunately, a sizeable number of such “interesting” specifications discovered by frequent pattern mining may not capture the correct use patterns of method calls. Consequently, when used in software testing or verification, these mined specifications lead to many false positive defects, which in turn consume much effort for manual investigation. We present a novel framework for automatically discovering legitimate specifications from execution traces using a mutation testing based approach. Such an approach gives a semantics bearing to the legitimacy of the discovered specifications. We introduce the notion of maximal precision and completeness as the desired forms of discovered specifications, and describe in detail suppression techniques that aid efficient discovery. Preliminary evaluation of this approach on several open source software projects shows that specifications discovered through our approach, compared with those discovered through frequent pattern mining, are much more precise and complete. When used in finding bugs, our specifications also locate defects with significantly fewer false positives and more true positives.

Dynamic specification mining involves discovering software behavior from traces for the purpose of program comprehension and bug detection. However, mining program behavior from execution traces is difficult for concurrent/distributed programs. Specifically, the inherent partial order relationships among events occurring across processes pose a big challenge to specification mining. In this paper, we propose a framework for mining partial orders so as to understand concurrent program behavior. Our miner takes in a set of concurrent program traces, and produces a message sequence graph (MSG) to represent the concurrent program behavior. An MSG represents a graph where the nodes of the graph are partial orders, represented as Message Sequence Charts. Mining an MSG allows us to understand concurrent program behaviors since the nodes of the MSG depict important "phases" or "interaction snippets" involving several concurrently executing processes. To demonstrate the power of this technique, we conducted experiments on mining behaviors of several fairly complex distributed systems. We show that our miner can produce the corresponding MSGs with both high precision and recall.

It has been a common practice nowadays to employ third-party libraries in software projects. Software libraries encapsulate a large number of useful, well-tested and robust functions, so that they can help improve programmers' productivity and program quality. To interact with libraries, programmers only need to invoke Application Programming Interfaces (APIs) exported from libraries. However, programmers do not always use libraries as effectively as expected in their application development. One commonly observed phenomenon is that some library behaviors are re-implemented by client code. Such re-implementation, or imitation, is not just a waste of resource and energy, but its failure to abstract away similar code also tends to make software error-prone. In this paper, we propose a novel approach based on trace subsumption relation of data dependency graphs to detect imitations of library APIs for achieving better software maintainability. Furthermore, we have implemented a prototype of this approach and applied it to ten large real-world open-source projects. The experiments show 313 imitations of explicitly imported libraries with high precision average of 82%, and 116 imitations of static libraries with precision average of 75%.

In a bug tracking system, different testers or users may submit multiple reports on the same bugs, referred to as duplicates, which may cost extra maintenance efforts in triaging and fixing bugs. In order to identify such duplicates accurately, in this paper we propose a retrieval function (REP) to measure the similarity between two bug reports. It fully utilizes the information available in a bug report including not only the similarity of textual content in summary and description fields, but also similarity of non-textual fields such as product, component, version, etc. For more accurate measurement of textual similarity, we extend BM25F - an effective similarity formula in information retrieval community, specially for duplicate report retrieval. Lastly we use a two-round stochastic gradient descent to automatically optimize REP for specific bug repositories in a supervised learning manner. We have validated our technique on three large software bug repositories from Mozilla, Eclipse and OpenOffice. The experiments show 10-27% relative improvement in recall rate@k and 17-23% relative improvement in mean average precision over our previous model. We also applied our technique to a very large dataset consisting of 209,058 reports from Eclipse, resulting in a recall rate@k of 37-71% and mean average precision of 47%.

Billions of dollars are spent annually on software-related cost. It is estimated that up to 45 percent of software cost is due to the difficulty in understanding existing systems when performing maintenance tasks (i.e., adding features, removing bugs, etc.). One of the root causes is that software products often come with poor, incomplete, or even without any documented specifications. In an effort to improve program understanding, Lo et al. have proposed iterative pattern mining which outputs patterns that are repeated frequently within a program trace, or across multiple traces, or both. Frequent iterative patterns reflect frequent program behaviors that likely correspond to software specifications. To reduce the number of patterns and improve the efficiency of the algorithm, Lo et al. have also introduced mining closed iterative patterns, i.e., maximal patterns without any superpattern having the same support. In this paper, to technically deepen research on iterative pattern mining, we introduce mining iterative generators, i.e., minimal patterns without any subpattern having the same support. Iterative generators can be paired with closed patterns to produce a set of rules expressing forward, backward, and in-between temporal constraints among events in one general representation. We refer to these rules as representative rules. A comprehensive performance study shows the efficiency of our approach. A case study on traces of an industrial system shows how iterative generators and closed iterative patterns can be merged to form useful rules shedding light on software design.

We present LM, a tool for mining scenario-based specifications in the form of Live Sequence Charts, a visual language that extends sequence diagrams with modalities. LM comes with a project management component, a wizard-like interface to the mining algorithm, a set of pre- and post-processing extensions, and a visualization module.

Bug repositories are usually maintained in software projects. Testers or users submit bug reports to identify various issues with systems. Sometimes two or more bug reports corre-spond to the same defect. To address the problem with du-plicate bug reports, a person called a triager needs to man-ually label these bug reports as duplicates, and link them to their ”master ” reports for subsequent maintenance work. However, in practice there are considerable duplicate bug re-ports sent daily; requesting triagers to manually label these bugs could be highly time consuming. To address this issue, recently, several techniques have be proposed using various similarity based metrics to detect candidate duplicate bug reports for manual verification. Au-tomating triaging has been proved challenging as two reports of the same bug could be written in various ways. There is still much room for improvement in terms of accuracy of du-plicate detection process. In this paper, we leverage recent advances on using discriminative models for information re-trieval to detect duplicate bug reports more accurately. We have validated our approach on three large software bug repositories from Firefox, Eclipse, and OpenOffice. We show that our technique could result in 17–31%, 22–26%, and 35– 43 % relative improvement over state-of-the-art techniques in OpenOffice, Firefox, and Eclipse datasets respectively using commonly available natural language information only.

Abstract The size-change principle devised by Lee, Jones and Ben-Amram, provides an effective method of determining program termination for recursive functions. It relies on a regular approximation to the call structure of the program, operates only over variables whose "size" is well-founded, and ignores the conditionals and return values in the program. The main contribution of our paper is twofold: firstly we improve size-change termination analysis by using better regular approximations to program flow, and secondly we extend the analysis beyond the original well-founded variables to include integer variables. In addition, we pay attention to program conditionals that are expressed by linear constraints and support the analysis of functions in which the return values are relevant to termination. Our analysis is entirely mechanical, exploits the decidability and expressive power of affine constraints and extends the set of programs that are size-change terminating.

There is a huge wealth of sequence data available, for example, customer purchase histories, program execution traces, DNA, and protein sequences. Analyzing this wealth of data to mine important knowledge is certainly a worthwhile goal. In this paper, as a step forward to analyzing patterns in sequences, we introduce the problem of mining closed repetitive gapped subsequences and propose efficient solutions. Given a database of sequences where each sequence is an ordered list of events, the pattern we would like to mine is called repetitive gapped subsequence, which is a subsequence (possibly with gaps between two successive events within it) of some sequences in the database. We introduce the concept of repetitive support to measure how frequently a pattern repeats in the database. Different from the sequential pattern mining problem, repetitive support captures not only repetitions of a pattern in different sequences but also the repetitions within a sequence. Given a user-specified support threshold min_sup, we study finding the set of all patterns with repetitive support no less than min_sup. To obtain a compact yet complete result set and improve the efficiency, we also study finding closed patterns. Efficient mining algorithms to find the complete set of desired patterns are proposed based on the idea of instance growth. Our performance study on various datasets shows the efficiency of our approach. A case study is also performed to show the utility of our approach.

Software is a ubiquitous component of our daily life. We often depend on the correct working of software systems. Due to the difficulty and complexity of software systems, bugs and anomalies are prevalent. Bugs have caused billions of dollars loss, in addition to privacy and security threats. In this work, we address software reliability issues by proposing a novel method to classify software behaviors based on past history or runs. With the technique, it is possible to generalize past known errors and mistakes to capture failures and anomalies. Our technique first mines a set of discriminative features capturing repetitive series of events from program execution traces. It then performs feature selection to select the best features for classification. These features are then used to train a classifier to detect failures. Experiments and case studies on traces of several benchmark software systems and a real-life concurrency bug from MySQL server show the utility of the technique in capturing failures and anomalies. On average, our pattern-based classification technique outperforms the baseline approach by 24.68% in accuracy.

Computation performed in many typical aspects involve side effects. In a purely functional setting, adding such aspects using techniques such as monadification will generally lead to crosscutting changes. This paper presents an approach to provide side-effecting aspects for purely lazy functional languages in a user transparent fashion. We propose a simple yet direct state manipulation construct for developing side-effecting aspects and devise a systematic monadification scheme to translate the woven code to a purely monadic style functional code.

Hard real-time systems are found in many critical embedded applications, for example aeroplane flight control, industrial production line control, and so on. The safe scheduling of tasks in these hard real-time systems is crucial to their correct operation, but the hard constraints of this type of scheduling reduce the responsiveness of the systems. In this paper we show the application of runtime analysis in informing the design of hard real-time embedded systems by allowing scheduled tasks to be dynamically re-ordered to improve the average responsiveness, while still meeting the hard constraints imposed by the system. The technique is semi-automated, and uses the reduce computer algebra system to precalculate a symbolic form of the runtime of scheduled tasks. The symbolic form is used to modify the source code of the scheduler.

Shared libraries have been prevalently deployed in many systems and application domains in the last decade. Their ubiquity depends largely on their allowance for sharing; ie., a single copy of the library is used across multiple applications running on a single system. Unfortunately, traditional partial evaluation does not consider the sharing issue. Specifically, libraries are treated as if they are statically linked, and sharing is not preserved during the process of creating and running specialized libraries, especially across different specialized applications. In this paper, we propose a methodology for run-time specialization that aims to maximize sharing during the whole specialization process. Specifically, we advocate a stand-alone specialization of shared libraries (independent of their clients), and propose a specialization mechanism which enables sharing of run-time specialized library code both within a specialized application and across multiple specialized applications. Our proposal includes a novel static transformation that constructs a generic specialization library/component, aiming to eliminate code duplication arising at compile-time, as well as a novel run-time specialization that eliminates code duplication occurring at run-time.

Sequential pattern mining first proposed by Agrawal and Srikant has received intensive research due to its wide range applicability in many real-life domains. Various improvements have been proposed which include mining a closed set of sequential patterns. Sequential patterns supported by the same sequences in the database can be considered as belonging to an equivalence class. Each equivalence class contains patterns partially-ordered by sub-sequence relationship and having the same support. Within an equivalence class, the set of maximal and minimal patterns are referred to as closed patterns and generators respectively. Generators used together with closed patterns can provide additional information which closed patterns alone are not able to provide. Also, as generators are the minimal members, they are preferable over closed patterns for model selection and classification based on the Minimum Description Length (MDL) principle. Several algorithms have been proposed for mining closed sequential patterns, but none so far for mining sequential generators. This paper fills this research gap by investigating properties of sequential generators and proposing an algorithm to efficiently mine sequential generators. The algorithm works on a three-step process of search space compaction, non-generator pruning and a final filtering step. We also introduce ranking of mined generators and propose mining of a unique generator per equivalence class. Performance study has been conducted on various synthetic and real benchmark datasets. They show that mining generators can be as fast as mining closed patterns even at low support thresholds.

Software specifications are often lacking, incomplete and outdated in the industry. Lack and incomplete specifications cause various software engineering problems. Studies have shown that program comprehension takes up to 45% of software development costs. One of the root causes of the high cost is the lack-of documented specification. Also, outdated and incomplete specification might potentially cause bugs and compatibility issues. In this paper, we describe novel data mining techniques to mine or reverse engineer these specifications from the pool of software engineering data. A large amount of software data is available for analysis. One form of software data is program execution traces. A program trace can be viewed as a sequence of events collected when a program is run. A set of program traces in turn can be viewed as a sequence database. In this paper, we present some novel work in mining software specifications by employing novel pattern mining and rule mining techniques. Performance studies show the scalability of our technique. Case studies on traces of a real industrial application show the utility of our technique in recovering program specifications from execution traces.

Abstract Software evolution incurs difficulties in program comprehension and software verification, and hence it increases the cost of software maintenance. In this study, we propose a novel technique to mine from program execution traces a sound and complete set of statistically significant temporal rules of arbitrary lengths. The extracted temporal rules reveal invariants that the program observes, and will consequently guide developers to understand the program behaviors, and facilitate all downstream applications such as verification and debugging. Different from previous studies that were restricted to mining two‐event rules (e.g., 〈lock〉→〈unlock〉), our algorithm discovers rules of arbitrary lengths. In order to facilitate downstream applications, we represent the mined rules as temporal logic expressions, so that existing model checkers or other formal analysis toolkit can readily consume our mining results. Performance studies on benchmark data sets and a case study on an industrial system have been performed to show the scalability and utility of our approach. We performed case studies on JBoss application server and a buggy concurrent versions system application, and the result clearly demonstrates the usefulness of our technique in recovering underlying program designs and detecting bugs. Copyright © 2008 John Wiley & Sons, Ltd.

Specification mining is a dynamic analysis process aimed at automatically inferring suggested specifications of a program from its execution traces. We describe a novel method, framework, and tool, for mining inter-object scenario-based specifications in the form of a UML2-compliant variant of Damm and Harels Live Sequence Charts (LSC). LSC extends the classical partial order semantics of sequence diagrams with temporal liveness and symbolic class level lifelines, in order to generate compact and expressive specifications. The output of our algorithm is a sound and complete set of statistically significant LSCs (i.e., satisfying given thresholds of support and confidence), mined from an input execution trace. We locate statistically significant LSCs by exploring the search space of possible LSCs and checking for their statistical significance. In addition, we use an effective search space pruning strategy, specifically adapted to LSCs, which enables efficient mining of scenarios of arbitrary size. We demonstrate and evaluate the utility of our work in mining informative specifications using a case study on Jeti, a popular, full featured messaging application

Studies have shown that program comprehension takes up to 45% of software development costs. Such high costs are caused by the lack-of documented specification and further aggravated by the phenomenon of software evolution. There is a need for automated tools to extract specifications to aid program comprehension. In this paper, a novel technique to efficiently mine common software temporal patterns from traces is proposed. These patterns shed light on program behaviors, and are termed iterative patterns. They capture unique characteristic of software traces, typically not found in arbitrary sequences. Specifically, due to loops, interesting iterative patterns can occur multiple times within a trace. Furthermore, an occurrence of an iterative pattern in a trace can extend across a sequence of indefinite length. Since a program behavior can be manifested in numerous ways, analyzing a single trace will not be sufficient. Iterative pattern mining extends sequential pattern and episode minings to discover frequent iterative patterns which occur repetitively both within a program trace and across multiple traces. In this paper, we present CLIPER (CLosed Iterative Pattern minER) to efficiently mine a closed set of iterative patterns. A performance study on several simulated and real datasets shows the efficiency of our mining algorithm and effectiveness of our pruning strategy. Our case study on JBoss Application Server confirms the usefulness of mined patterns in discovering interesting software behavioral specification.

Component-based software development advocates the reuse of generic off-the-shelf components to build complex and reliable applications. Unfortunately, the genericness of components results in degradation of system performance. Little progress has been made in promoting the specialization of a component independent of its use context. In this paper we propose a component specialization framework aiming at producing reusable specialization component which are adaptive to different specialization contexts. We advocate profitability declaration, a novel methodology to capture specialization opportunities independent of how components are deployed. This conceptual profitability declaration is translated into a profitability signature in the form of the binding-time constraint. A profitable specialization component, PSC for short, is then developed, aiming to be deployed in various applications in place of the original generic component, as well as to be adaptive to different specialization contexts. In addition to the merit of reusability, PSC also achieves a reasonable balance between multiplicity of specialized codes and the space required for keeping them. We believe that our framework will promote the usage of program specialization in component-based software development.

10.1145/1167473.1167498

Recursive programs may require large numbers of procedure calls and stack operations, and many such recursive programs exhibit exponential time complexity, due to the time spent re-calculating already computed sub-problems. As a result, methods which transform a given recursive program to an iterative one have been intensively studied. We propose here a new framework for transforming programs by removing recursion. The framework includes a unified method of deriving low time-complexity programs by solving recurrences extracted from the program sources. Our prototype system, APTSR1, is an initial implementation of the framework, automatically finding simpler "closed form" versions of a class of recursive programs. Though in general the solution of recurrences is easier if the functions have only a single recursion parameter, we show a practical technique for solving those with multiple recursion parameters.

Aspect-oriented programming (AOP) has been shown to be a useful model for software development. Special care must be taken when we try to adapt AOP to strongly typed functional languages which come with features like a type inference mechanism, polymorphic types, higher-order functions and type-scoped pointcuts. Our main contribution lies in a seamless integration of these two paradigms through a static weaving process which deals with around advices with type-scoped pointcuts in the presence of higher-order functions. We give a source-level type inference system for a higher-order, polymorphic language coupled with type-scoped pointcuts. The type system ensures that base programs are oblivious to the type of around advices. We present a type-directed translation scheme which resolves all advice applications at static time. The translation removes advice declarations from source programs and produces translated code which is typable in the Hindley-Milner system.

Improper management of software evolution, compounded by imprecise, and changing requirements, along with the "short time to market" requirement, commonly leads to a lack of up-to-date specifications. This can result in software that is characterized by bugs, anomalies and even security threats. Software specification mining is a new technique to address this concern by inferring specifications automatically. In this paper, we propose a novel API specification mining architecture called SMArTIC Specification Mining Architecture with Trace fIltering and Clustering) to improve the accuracy, robustness and scalability of specification miners. This architecture is constructed based on two hypotheses: (1) Erroneous traces should be pruned from the input traces to a miner, and (2) Clustering related traces will localize inaccuracies and reduce over-generalizationin learning. Correspondingly, SMArTIC comprises four components: an erroneous-trace filtering block, a related-trace clustering block, a learner, and a merger. We show through experiments that the quality of specification mining can be significantly improved using SMArTIC.

Many software properties can be analysed through a relational size analysis on each function's inputs and outputs. Such relational analysis (through a form of dependent typing) has been successfully applied to declarative programs, and to restricted imperative programs; but it has been elusive for object-based programs. The main challenge is that objects may mutate and they may be aliased. In this paper, we show how safety policies of programs can be analysed by tracking size properties of objects and be enforced by objects' invariants and the preconditions of methods. We propose several new ideas to allow both mutability and sharing of objects, whilst aiming for precision in our analysis. We introduce the concept of size-immutability to facilitate sharing, and also a set of alias controls to track unaliased objects whose size properties may change. We formalise our results through a set of advanced type checking rules for an object-based imperative language. We re-affirm the utility of the proposed type system by showing how a variety of software properties can be automatically verified according to size-inspired safety policies.

Most research on automated specification-based software testing has focused on the automated generation of test cases. Before a software system can be tested, it must be set up according to the input requirements of the test cases. This setup process is usually performed manually, especially when testing complex data structures and databases. After the system is properly set up, a test execution tool runs the system according to the test cases and pre-recorded test scripts to obtain the outputs, which are evaluated by a test evaluation tool. This paper complements the current research on automated specification-based testing by proposing a scheme that combines the setup process, test execution, and test validation into a single test program for testing the behavior of object-oriented classes. The test program can be generated automatically given the desired test cases and closed specifications of the classes. With closed specifications, every class method is defined in terms of other methods which are, in turn, defined in their own class specifications. The core of the test program generator is a partial-order planner which plans the sequence of instructions required in the test program. The planner is, in turn, implemented as a tree-search algorithm. It makes function calls to the Omega Calculator library, which solves the constraints given in the test cases. A first-cut implementation of the planner has been completed, which is able to handle simple arithmetics and existential quantifications in the class specifications. A soundness and completeness proof sketch of the planner is also provided in this paper.

Many program optimizations and analyses, such as array-bounds checking, termination analysis, depend on knowing the size of a function's input and output. However, size information can be difficult to compute. Firstly, accurate size computation requires detecting a size relation between different inputs of a function. Secondly, size information may also be contained inside a collection (data structure with multiple elements). In this paper, we introduce some techniques to derive universal and existential size properties over collections of elements of recursive data structures. We shall show how a mixed constraint system could support the enhanced size type, and highlight examples where collection analysis are useful.

A divide and conquer strategy enables a problem to be divided into subproblems, which are solved independently and later combined to form solutions of the original problem. For solving constraint satisfaction problems, however, the divide and conquer technique has not been shown to be effective. This is because it is not possible to cleanly divide a problem into independent subproblems in the presence of constraints that involve variables belonging to different subproblems. Consequently, solutions of one subproblem may prune solutions of another subproblem, making those solutions of the latter subproblem redundant. In this paper we propose a divide and conquer approach to constraint solving in a lazy evaluation framework. In this framework, a subproblem is solved on demand, which eliminates redundant consistency checks. Moreover, once solved, the solutions of a subproblem can be reused in the satisfaction of various global constraints connecting this subproblem with others, thus reducing the search space. We also demonstrate the effectiveness of our algorithm in solving a practical problem: finding all instances of a user-defined pattern in stock market price charts.

10.1145/507635.507653

Many program optimisations and analyses, such as arraybound checking, termination analysis, etc, depend on knowing the size of a function's input and output. However, size information can be difficult to compute. Firstly, accurate size computation requires detecting size relation between different inputs of a function. Secondly, different optimisations and analyses may require slightly different size information, and thus slightly different computation. Literature in size computation has mainly concentrated on size checking, instead of inferencing. In this paper, we provide a generic framework on which different size variants can be expressed and computed. We also describe an effective algorithm for inferring, instead of checking, size information. Size information are expressed in terms of Presburger formulae, and our algorithm utilises the Omega Calculator to compute as exact a size information as possible, within the linear arithmetic capability. 1 Introduction Many program optimi...

Abstract This paper presents semantic specifications and correctness proofs for both on-line and offline partial evaluation of strict first-order functional programs. To do so, our strategy consists of defining a core semantics as a basis for the specification of three non-standard evaluations: instrumented evaluation, on-line and off-line partial evaluation. We then use the technique of logical relations to prove the correctness of both on-line and off-line partial evaluation semantics. The contributions of this work are as follows: 1. We provide a uniform framework to defining and proving correct both on-line and off-line partial evaluation. 2. This work required a formal specification of on-line partial evaluation with polyvariant specialization. We define criteria for its correctness with respect to an instrumented standard semantics. As a by-product, on-line partial evaluation appears to be based on a fixpoint iteration process, just like binding-time analysis. 3. We show that binding-time analysis, the preprocessing phase of off-line partial evaluation, is an abstraction of on-line partial evaluation. Therefore, its correctness can be proved with respect to on-line partial evaluation, instead of with respect to the standard semantics, as is customarily done. 4. Based on the binding-time analysis, we formally derive the specialization semantics for off-line partial evaluation. This strategy ensures the correctness of the resulting semantics.

article Free AccessParameterized partial evaluation Authors: Charles Consel Yale University Yale UniversityView Profile , Siau Cheng Khoo Yale University Yale UniversityView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 15Issue 3pp 463–493https://doi.org/10.1145/169683.174155Published:01 July 1993Publication History 47citation352DownloadsMetricsTotal Citations47Total Downloads352Last 12 Months11Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

article Free Access Share on Compiling inheritance using partial evaluation Authors: Siau Cheng Khoo Yale University, Department of Computer Science, New Haven, CT Yale University, Department of Computer Science, New Haven, CTView Profile , R. S. Sundaresh Yale University, Department of Computer Science, New Haven, CT Yale University, Department of Computer Science, New Haven, CTView Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 26Issue 9Sept. 1991 pp 211–222https://doi.org/10.1145/115866.115886Online:01 May 1991Publication History 13citation231DownloadsMetricsTotal Citations13Total Downloads231Last 12 Months6Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

article Free Access Share on Parameterized partial evaluation Authors: Charles Consel Yale University, Department of Computer Science, New Haven, CT Yale University, Department of Computer Science, New Haven, CTView Profile , Siau Cheng Khoo Yale University, Department of Computer Science, New Haven, CT Yale University, Department of Computer Science, New Haven, CTView Profile Authors Info & Claims ACM SIGPLAN NoticesVolume 26Issue 6June 1991 pp 92–106https://doi.org/10.1145/113446.113454Online:01 May 1991Publication History 7citation244DownloadsMetricsTotal Citations7Total Downloads244Last 12 Months6Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF