Abstract Function contract generation is a classical problem in program analysis that targets the automated analysis of functions in a program with multiple procedures. The problem is fundamental in interprocedural analysis where properties of functions are first obtained via the generation of function contracts and then the generated contracts are used as building blocks to analyze the whole program. Typical objectives in function contract generation include pre-/post-conditions and assigns information (that specifies the modification information over program variables and memory segments during function execution). In programs with array manipulations, a crucial point in function contract generation is the treatment of array segments that imposes challenges in inferring invariants and assigns information over such segments. To address this challenge, we propose a novel symbolic execution framework that carries invariants and assigns information over contiguous segments of arrays. We implement our framework as a prototype within LLVM, and further integrate our prototype with the ANSI/ISO C Specification Language (ACSL) assertion format and the Frama-C software verification platform. Experimental evaluation over a variety of benchmarks from the literature and functions from realistic libraries shows that our framework is capable of handling array manipulating functions that indeed involve the carry of array information and are beyond existing approaches.

Zero-knowledge proof (ZKP) systems have surged attention and held a fundamental role in contemporary cryptography. Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This article introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the computer algebra system . The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC 4 , is proposed to represent the implementation of the method. Experiments show that AC 4 demonstrates an increase in the solved rate, showing a 36.7% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.

Large language models (LLMs) are increasingly used as evaluators in natural language generation tasks, offering advantages in scalability and interpretability over traditional evaluation methods.However, existing LLMbased evaluations often suffer from biases and misalignment, particularly in domain-specific tasks, due to limited functional understanding and knowledge gaps.To address these challenges, we first investigate the relationship between an LLM-based evaluator's familiarity with the target task and its evaluation performance.We then introduce the Co-Eval framework, which leverages a criteria planner model and optimized machine metrics to enhance the scalability and fairness of LLMbased evaluation.Experimental results on both general and domain-specific tasks demonstrate that Co-Eval reduces biases, achieving up to a 0.4903 reduction in self-preference bias, and improves alignment with human preferences, with gains of up to 0.324 in Spearman correlation.

Minyu Chen, Guoqiang Li, Ling-I Wu, Ruibang Liu. Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers). 2025.

Abstract In the realm of blockchains, synchronization challenges are two-folded. First, smart contracts from different blockchains cannot communicate with each other, making it hard to establish a trustworthy communication channel to share and maintain a universal state between each other. Second, transactions on different blockchains can hardly be ordered. Hence interference is expected. We need a novel way to handle interference. Traditional solutions involving third parties have safety and liveness issues and thus compromise between safety, permissionless, and liveness. ZK Multi-Blockchain Aggregatoris a multi-blockchain execution layer that leverages the power of zero-knowledge proof to minimize the trust base of multi-blockchain communication, which does not compromise safety, liveness, permissionless, and atomicity. In contrast to traditional blockchain bridges performing transactions on different blockchains separately and using a relay system to enforce the order of transactions and prevent interference, our method uses an entirely new approach, such that for each multi-blockchain transaction, it simulates the multi-blockchain transaction in its aggregator chain. Our aggregator uses zero-knowledge proofs of the simulation to convince involved blockchains to update their local state accordingly. On top of this layer, rich applications over multi-blockchains can run safely and efficiently.

Due to the general undecidable results, verification of concurrent programs is a big challenge. Most existing verifiers adopt Petri net and its extensions based on abstraction and approximation as their verification models, which yet suffer from intractable complexity and are thus challenging to be efficient and complete. We choose Basic Parallel Process (BPP) , a subclass of Petri nets, as the backbone verification model for verifying concurrent programs due to its lower complexity. We propose BPPChecker, the first model checker for verifying a subclass of CTL on BPP. A constraint-based algorithm is given in which formulas are handled by SMT solver Z3. Our approach involves introducing a k -step semantics for the EG operator. By doing so, we reduce the problem of deciding the satisfiability of EG -formulas and EF 1 -formulas to the problem of deciding the satisfiability of linear integer arithmetic formulas. Besides, we encode the Actor Communicating System (ACS) , a program model for asynchronously communicating programs, to BPP. Experimental results show that BPPChecker performs more efficiently than the existing tools for a series of branching-time property verification problems of Erlang programs.

The communities of blockchains and distributed ledgers have been stirred up by the introduction of zero-knowledge proofs (ZKPs). Originally designed as a solution to privacy issues, ZKPs have now evolved into an effective remedy for scalability concerns. To enable ZKPs, Rank-1 Constraint Systems (R1CSs) offer a verifier for bilinear equations. In order to accurately and efficiently represent R1CSs, several language tools, such as Circom, Noir, and Snarky, have been proposed to automate the compilation of advanced programs into R1CSs. However, due to the flexible nature of R1CS representation, there can be significant differences in the compiled R1CS forms generated from circuit language programs with the same underlying semantics. To address this issue, this article puts forth a dataflow-based R1CS paradigm algorithm, which produces a standardized format for different R1CS instances with identical semantics. Additionally, we present an R1CS benchmark, and our experimental evaluation demonstrates the efficacy of our methods.

WebAssembly, or WASM for short, is a binary code format for a stack-based virtual machine, first published in 2018 and now becomes a main-steam technology for providing distributed serverless functions. Recently, the demand for privacy and trustless serverless functions has started to grow in cloud, edge, and grid computing, which poses a question for those serverless function providers: how they ensure trustworthy computation in safety-critical scenarios like financial systems, cybersecurity, private data handling, etc. To address this, we leverage the technology ZKSNARK (zero-knowledge Succinct Non-interactive Argument of Knowledge), a powerful proof system that allows efficient verification of the evaluation problem of statements, to give WASM runtime the ability to provide trustless computation service. More precisely, we present ZKWASM, a ZKSNARK backed virtual machine that emulates the execution of WASM bytecode and generates zero-knowledge-proofs for the emulation result. The proof generated by the ZKWASM virtual machine can then be used to convince an entity, with no leakage of confidential information, that the result of the emulation enforces the semantic specification of WASM.

The rapid development of deep learning has significantly transformed the ecology of the software engineering field. As new data continues to grow and evolve at an explosive rate, the challenge of iteratively updating software built on neural networks has become a critical issue. While the continuous learning paradigm enables networks to incorporate new data and update accordingly without losing previous memories, resulting in a batch of new networks as candidates for software updating, these approaches merely select from these networks by empirically testing their accuracy; they lack formal guarantees for such a batch of networks, especially in the presence of adversarial samples. Existing verification techniques, based on constraint solving, interval propagation, and linear approximation, provide formal guarantees but are designed to verify the properties of individual networks rather than a batch of networks. To address this issue, we analyze the batch verification problem corresponding to several non-traditional machine learning paradigms and further propose a framework named HOBAT (BATch verification for HOmogeneous structural neural networks) to enhance batch verification under reasonable assumptions about the representation of homogeneous structure neural networks, increasing scalability in practical applications. Our method involves abstracting the neurons at the same position in a batch of networks into a single neuron, followed by an iterative refinement process on the abstracted neuron to restore the precision until the desired properties for verification are met. Our method is orthogonal to boundary propagation verification on a single neural network. To assess our methodology, we integrate it with boundary propagation verification and observe significant improvements compared to the vanilla approach. Our experiments demonstrate the enormous potential for verifying large batches of networks in the era of big data.

The introduction of zero-knowledge proofs (ZKPs) has had a profound impact on the blockchain and distributed ledger communities. ZKPs require the utilization of Rank-1 Constraint Systems (R1CS), which serve as verifiers for bi-linear equations. However, the flexibility of R1CS representation leads to notable variations in the compiled R1CS forms derived from circuit language programs with identical semantics. To tackle this challenge, this paper proposes a data-flow-based R1CS paradigm algorithm, producing a standardized format for different R1CS instances with the identical semantics. By adopting the normalized R1CS format circuits, the complexity of circuits’ verification can be reduced. Furthermore, this paper presents an R1CS normalization algorithm benchmark, and our experimental evaluation demonstrates the effectiveness and accuracy of our methods.

Open-source platforms such as GitHub and Stack Overflow both play significant roles in current software ecosystems. It is crucial but time-consuming for developers to raise programming questions in coding forums such as Stack Overflow and be navigated to actual solutions on GitHub repositories. In this paper, we dedicate to accelerating this activity. We find that traditional information retrieval-based methods fail to handle the long and complex questions in coding forums, and thus cannot find suitable coding repositories. To effectively and efficiently bridge the semantic gap between repositories and real-world coding questions, we introduce a specialized dataset named Repo4QA, which includes over 12,000 question-repository pairs constructed from Stack Overflow and GitHub. Furthermore, we propose QuRep, a CodeBERT-based model that jointly learns the representation of both questions and repositories. Experimental results demonstrate that our model simultaneously captures the semantic features in both questions and repositories through supervised contrastive loss and hard negative sampling. We report that our approach outperforms existing state-of-art methods by 3%-8% on MRR and 5%-8% on P@1.

Invariant generation is a classical problem to automatically generate invariants to aid the formal analysis of programs. In this work, we consider the problem of generating tight linear-invariants over affine programs (i.e., programs with affine guards and updates) without a prescribed goal property. In the literature, the only known sound and complete characterization to solve this problem is via Farkas’ Lemma (FL), and has been implemented through either quantifier elimination or reasonable heuristics. Although FL-based approaches can generate highly accurate linear invariants from the completeness of FL, the main bottleneck to applying these approaches is the scalability issue caused by either non-linear constraints or combinatorial explosion. We base our approach on the only practical FL-based approach [Sankaranarayanan ‍ et al. , SAS 2004] that applies FL with reasonable heuristics, and develop two novel and independent improvements to leverage the scalability. The first improvement is the novel idea to generate invariants at one program location in a single invariant-generation process, so that the invariants for each location are generated separately rather than together in a single computation. This idea naturally leads to a parallel processing that divides the invariant-generation task for all program locations by assigning the locations separately to multiple processors. Moreover, the idea enables us to develop detailed technical improvements to further reduce the combinatorial explosion in the original work [Sankaranarayanan ‍ et al. , SAS 2004]. The second improvement is a segmented subsumption testing in the CNF-to-DNF expansion that allows discovering more local subsumptions in advance. We formally prove that our approach has the same accuracy as the original work and thus does not incur accuracy loss on the generated invariants. Moreover, experimental results on representative benchmarks involving non-trivial linear invariants demonstrate that our approach improves the runtime of the original work by several orders of magnitude, even in the non-parallel scenario that sums up the execution time for all program locations. Hence, our approach constitutes the first significant improvement in FL-based approaches for linear invariant generation after almost two decades.

Haze seriously affects the reliability of industrial systems, especially vision-based outdoor industrial systems such as autopilot systems. A majority of existing dehazing methods are not specifically designed for industrial systems and do not consider the reliability and resource cost of industrial system implementation. In this article, a novel meta-attention dehazing network (MADN) is proposed for direct restoration of clear images from hazy images without using the physical scattering model. Combined with parallel operation and enhancement modules, the meta-network automatically selects the most suitable dehazing network structure based on the current input hazy image by a meta-attention module. In addition, a novel feature loss calculated by the meta-network is proposed, which can accelerate the convergence of the dehazing network to meet the application requirements of practical industrial systems. A large number of experimental results on synthetic and real-world datasets show that the proposed MADN satisfies the needs of industrial systems.

This paper presents a formal approach for modelling and reasoning about information flow control in software systems under Hoare and He's Unifying Theories of Programming (UTP). We investigate the problem of integrating information flow control into system design in a unified semantic setting. Our approach can therefore treat information flow analysis and control in various families of specification languages and programming paradigms in a more general way. In addition, we formalise the link between classes of predicates as a paired function which maps set of the predicates from one class into set of the predicates from the other with a concern of flow security preservation. The proposed flow-sensitive combined theories of multiple level classes of predicates can be applied to ensure flow security in different paradigms under stepwise development.

Knowledge graphs are used extensively in various fields. Labor-intensive and time-consuming error detection for large-scale knowledge graphs significantly increases the need for efficient model checking algorithms in large-scale graphs. Since conventional algorithms are inefficient on such graphs, we propose a new liveness algorithm of knowledge graphs, under a specific given set of labels. By trimming and marking the graphs alternately, a weakly connected components algorithm is then designed to separate graphs into several disjoint sets and a bidirectional forward-backward algorithm computes strongly connected components in each set in parallel. We have implemented our algorithm on a real medical knowledge graph and several open data sets. The evaluation shows that our algorithm achieves up to 11.2x speedup over conventional algorithm with 16 threads.

Many Q&A sites initially run only in English, and then gradually release their multi-lingual variants to serve users who speak other languages. The launch of such multi-lingual sites always lead to an intense dispute about the pros and cons of multi-lingual sites. Although all arguments and concerns sound reasonable, people can rarely provide solid evidence to convince each other. In this paper, from users' comments about the launch of several non-English Stack Overflow sites, we first identify three major concerns including community split, knowledge needs and interests in other languages, and knowledge fragmentation and duplication. To validate these three concerns, we conduct an evidence-based data analysis and comparison of user characteristics, tag usage and cross-site links between the Russian Stack Overflow and the English Stack Overflow on these three concerns. Our study sheds light on the existence value and risks of multi-lingual Q&A sites.

Tagging is a defining characteristic of Web 2.0. It allows users of social computing systems (e.g., question and answering (Q&A) sites) to use free terms to annotate content. However, is tagging really a free action? Existing work has shown that users can develop implicit consensus about what tags best describe the content in an online community. However, there has been no work studying the regularities in how users order tags during tagging. In this paper, we focus on the natural ordering of tags in domain-specific Q&A sites. We study tag sequences of millions of questions in four Q&A sites, i.e., CodeProject, SegmentFault, Biostars, and CareerCup. Our results show that users of these Q&A sites can develop implicit consensus about in which order they should assign tags to questions. We study the relationships between tags that can explain the emergence of natural ordering of tags. Our study opens the path to improve existing tag recommendation and Q&A site navigation by leveraging the natural ordering of tags.

A sheer number of techniques and web resources are available for software engineering practice and this number continues to grow. Discovering semantically similar or related technical terms and web resources offers the opportunity to design appealing services to facilitate information retrieval and information discovery. In this study, we extract technical terms and web resources from a community of question and answer (Q&A) discussions and propose an approach based on a neural language model to learn the semantic representations of technical terms and web resources in a joint low-dimensional vector space. Our approach maps technical terms and web resources to a semantic vector space based only on the surrounding technical terms and web resources of a technical term (or web resource) in a discussion thread, without the need for mining the text content of the discussion. We apply our approach to Stack Overflow data dump of March 2018. Through both quantitative and qualitative analyses in the clustering, search, and semantic reasoning tasks, we show that the learnt technical-term and web-resource vector representations can capture the semantic relatedness of technical terms and web resources, and they can be exploited to support various search and semantic reasoning tasks, by means of simple K -nearest neighbor search and simple algebraic operations on the learnt vector representations in the embedding space.

Application Programming Interfaces (APIs) have been widely discussed on social-technical platforms (e.g., Stack Overflow). Extracting API mentions from such informal software texts is the prerequisite for API-centric search and summarization of programming knowledge. Machine learning based API extraction has demonstrated superior performance than rule-based methods in informal software texts that lack consistent writing forms and annotations. However, machine learning based methods have a significant overhead in preparing training data and effective features. In this paper, we propose a multi-layer neural network based architecture for API extraction. Our architecture automatically learns character-, word- and sentence-level features from the input texts, thus removing the need for manual feature engineering and the dependence on advanced features (e.g., API gazetteers) beyond the input texts. We also propose to adopt transfer learning to adapt a source-library-trained model to a target-library, thus reducing the overhead of manual training-data labeling when the software text of multiple programming languages and libraries need to be processed. We conduct extensive experiments with six libraries of four programming languages which support diverse functionalities and have different API-naming and API-mention characteristics. Our experiments investigate the performance of our neural architecture for API extraction in informal software texts, the importance of different features, the effectiveness of transfer learning. Our results confirm not only the superior performance of our neural architecture than existing machine learning based methods for API extraction in informal software texts, but also the easy-to-deploy characteristic of our neural architecture.

Dynamic emotion is typically used to facilitate human–machine interactions. Conversational data from social media contain a considerable amount of useful information, and such data are the foundation for researching dynamic and artificial emotion. At present, most human–machine interaction systems focus on the complexity and accuracy of the dialog but neglect the emotional characteristics of the speaker. When generating a dialog considering the emotional personality of the interlocutor, controlling, and guiding the dialog to a specified direction are essential. This article presents a system for studying dynamic emotions in human-computer interaction from the perspective of emotional transfer and guidance. Based on the emotional state of the interlocutor and the distribution of emotional transfer, the process of emotional transfer is simulated and sampled, and the sequence of emotional guidance is generated. In this system, two algorithms are proposed. A generative Markov chain Monte Carlo (GEN-MCMC) algorithm is proposed to generate a variety of emotional transfer sequences that fit the talke’s personality dynamically based on the real-world dialog. Further, a guiding MCMC (GUI-MCMC) algorithm-based GEN-MCMC is proposed to generate the emotional guiding sequences. The generated emotional sequences by GEN-MCMC were evaluated in two aspects: 1) consistency and 2) diversity. The experimental results show that the GEN-MCMC algorithm performs better than the general sequence generation algorithm in terms of consistency and diversity in generating emotional states. The GUI-MCMC was able to generate a proper stimulus sequence when given the first and target emotions. An emotional stimulus sequence can simulate the emotional transfer of the interlocutor in the process of dialogue, and give the observer appropriate reference to guide and control the emotions of dialogue. The experimental results show that the proposed system can effectively model the dynamic emotion in emotional transfer and guidance, which can be further used to build chat robots, intelligent assistants, and human–machine interaction systems. The models can also be used for emotional induction and enhance the feel-good or feel-terrible factor in human–machine communication applications, such as medical treatment of mental diseases, interrogation, and psychological attack and defense.

The selection of cloud resources is important to users which influences their utility directly. To improve the users’ utility of purchased resources, according to the historical bidding information, we present data-driven cloud resource procurement (CRP) auctions which can help the resource buyer make an optimized selection for cloud resources. First, we design two procurement auction mechanisms with personalized reserve prices for CRP: Lazy-CRP and Eager-CRP, in which the reserve prices are set by the broker before the auction based on the broker’s knowledge about costs of cloud providers. Then, given the assumption that each cloud provider is myopic, we propose the optimal learning algorithms of personalized reserve prices for the Lazy-CRP approach, and 2-approximation learning algorithm for the Eager-CRP approach. Both of two algorithms can be performed even if the cost distribution functions of cloud providers are nonidentical. By comparing our mechanisms with Vickery–Clark–Groves CRP (VCG-CRP) in simulation, the results show that our proposed mechanism is very suitable for occasions where the number of providers is very small. According to the results of the simulation, the total utilities obtained by the data-driven procurement schemes are significantly higher than VCG-CRP when the number of cloud providers is less than four. When there are only two providers, the increased total utility of our mechanism can be up to 80% of that obtained by VCG-CRP.

Statistical divergence is widely applied in multimedia processing, basically due to regularity and interpretable features displayed in data. However, in a broader range of data realm, these advantages may no longer be feasible, and therefore a more general approach is required. In data detection, statistical divergence can be used as a similarity measurement based on collective features. In this paper, we present a collective detection technique based on statistical divergence. The technique extracts distribution similarities among data collections, and then uses the statistical divergence to detect collective anomalies. Evaluation shows that it is applicable in the real world.

According to the World Health Organization(WHO), it is estimated that approximately 1.3 billion people live with some forms of vision impairment globally, of whom 36 million are blind. Due to their disability, engaging these minority into the society is a challenging problem. The recent rise of smart mobile phones provides a new solution by enabling blind users' convenient access to the information and service for understanding the world. Users with vision impairment can adopt the screen reader embedded in the mobile operating systems to read the content of each screen within the app, and use gestures to interact with the phone. However, the prerequisite of using screen readers is that developers have to add natural-language labels to the image-based components when they are developing the app. Unfortunately, more than 77% apps have issues of missing labels, according to our analysis of 10,408 Android apps. Most of these issues are caused by developers' lack of awareness and knowledge in considering the minority. And even if developers want to add the labels to UI components, they may not come up with concise and clear description as most of them are of no visual issues. To overcome these challenges, we develop a deep-learning based model, called LabelDroid, to automatically predict the labels of image-based buttons by learning from large-scale commercial apps in Google Play. The experimental results show that our model can make accurate predictions and the generated labels are of higher quality than that from real Android developers.

GUI animations, such as card movement, menu slide in/out, snackbar display, provide appealing user experience and enhance the usability of mobile applications. These GUI animations should not violate the platform's UI design guidelines (referred to as design-don't guideline in this work) regarding component motion and interaction, content appearing and disappearing, and elevation and shadow changes. However, none of existing static code analysis, functional GUI testing and GUI image comparison techniques can "see" the GUI animations on the scree, and thus they cannot support the linting of GUI animations against design-don't guidelines. In this work, we formulate this GUI animation linting problem as a multi-class screencast classification task, but we do not have sufficient labeled GUI animations to train the classifier. Instead, we propose an unsupervised, computer-vision based adversarial autoencoder to solve this linting problem. Our autoencoder learns to group similar GUI animations by "seeing" lots of unlabeled real-application GUI animations and learning to generate them. As the first work of its kind, we build the datasets of synthetic and real-world GUI animations. Through experiments on these datasets, we systematically investigate the learning capability of our model and its effectiveness and practicality for linting GUI animations, and identify the challenges in this linting problem for future work.

Detecting Graphical User Interface (GUI) elements in GUI images is a domain-specific object detection task. It supports many software engineering tasks, such as GUI animation and testing, GUI search and code generation. Existing studies for GUI element detection directly borrow the mature methods from computer vision (CV) domain, including old fashioned ones that rely on traditional image processing features (e.g., canny edge, contours), and deep learning models that learn to detect from large-scale GUI data. Unfortunately, these CV methods are not originally designed with the awareness of the unique characteristics of GUIs and GUI elements and the high localization accuracy of the GUI element detection task. We conduct the first large-scale empirical study of seven representative GUI element detection methods on over 50k GUI images to understand the capabilities, limitations and effective designs of these methods. This study not only sheds the light on the technical challenges to be addressed but also informs the design of new GUI element detection methods. We accordingly design a new GUI-specific old-fashioned method for non-text GUI element detection which adopts a novel top-down coarse-to-fine strategy, and incorporate it with the mature deep learning model for GUI text detection.Our evaluation on 25,000 GUI images shows that our method significantly advances the start-of-the-art performance in GUI element detection.

Summary Provenance is information about the origin and creation of data. In data science and engineering related with cloud environment, such information is useful and sometimes even critical. In data analytics, it is necessary for making data‐driven decisions to trace back history and reproduce final or intermediate results, even to tune models and adjust parameters in a real‐time fashion. Particularly, in cloud, users need to evaluate data and pipeline trustworthiness. In this paper, we propose a solution: LogProv, toward realizing these functionalities for big data provenance, which needs to renovate data pipelines or some of big data software infrastructure to generate structured logs for pipeline events, and then stores data and logs separately in cloud space. The data are explicitly linked to the logs, which implicitly record pipeline semantics. Semantic information can be retrieved from the logs easily since they are well defined and structured beforehand. We implemented and deployed LogProv in Nectar Cloud,* associated with Apache Pig, Hadoop ecosystem, and adopted Elasticsearch to provide query service. LogProv was evaluated and empirically case studied. The results show that LogProv is efficient since the performance overhead is no more than 10%; the query can be responded within 1 second; the trustworthiness is marked clearly; and there is no impact on the data processing logic of original pipelines.

Time series is very ubiquitous in both the industrial environment and real-life. Capturing the time dependency is very useful for time series analysis. Although the one-dimensional local binary pattern (1D-LBP) can analyze the Univariate time series, it cannot effectively handle the multivariate time series (MTS). The UTS can be considered as zero-order tensor time series (TTS), while the MTS can be considered as one- or higher order TTS. Each variable in MTS depends not only on its past values, but also on the other variables. In this article, we propose a temporal tensor LBP (TTLBP) operator to extract the discriminative temporal features from TTS by extending 1D-LBP operation from the scalar-wise to the tensor-wise. The TTLBP is discriminative and can handle the TTS effectively and straightforwardly. To the best of our knowledge, TTLBP is the first LBP variant for TTS analysis. Furthermore, we also propose a stricter uniform TTLBP to improve robustness and to reduce the high dimensionality. We apply the proposed TTLBP in the edge intelligence-assisted video anomaly detection system. Qualitative and quantitative comparisons demonstrate the effectiveness of the proposed TTLBP.

Vision systems are the core information collection module in outdoor industrial systems such as factory inspection robots. However, haze greatly reduces working efficiency. Existing dehazing methods have two problems-first, they are not specifically designed for the industrial systems; second, these methods include several assumptions in their design processes and imaging models, leading to unsatisfactory results. In this article, an approach for single image dehazing is proposed to improve the efficiency of outdoor vision-based systems. First, a novel haze imaging model is proposed based on the dichromatic atmospheric scattering model. It considers the effects of multiple scattering and involves fewer assumptions. Then a data-driven technique called sparse representation is used to solve this model. Considering a haze image, a distorted and blurred version of a fine image, every patch is presented using dedicatedly prepared over-complete dictionaries and is traced back to a haze-free image. Quantitative and qualitative comparisons on a number of real-world haze images demonstrate that the proposed approach not only is more stable but also leads to better dehazing results.

Internet of Things (IoT) has become a new paradigm of communication to reform traditional industries, in which distributed data automatically collected via IoT in a low cost enables many new IT services that were even impossible decades ago. This research reports on an IoT-enabled production management service for crude-oil industry. In practice, even if an optimal management decision is achieved, disruptions, such as possible oil-device failures, inclement weathers and other disturbances, arise frequently and then weaken efficiency and stability of supplement. With the help of IoT, a near-real-time management service comes into being, although the adoption of IoT brings new challenges to management of disruptions. The contributions of this article are as follows: First, a service framework is proposed for refinery which combines MQTT and Azure cloud, enabling reliable data/command delivery. Second, a smart disruption management service system is developed, which consists of monitor and alarm module, disruption management module, and rescheduling procedure module. The rescheduling procedure module takes into account the network of the refinery operations, and is easy to accommodate changes in the refinery configuration for unforeseen disruptions. The experimental results show that the proposed disruption management method balances efficiency and stability compared to traditional methods.

OSEK/VDX is a specification for vehicle-mounted systems. Currently, the specification has been widely adopted by many automotive companies to develop a distributed vehicle application system. However, the ever increasing complexity of the developed distributed application system has created a challenge for exhaustively ensuring its reliability. Model checking as an exhaustive technique has been applied to verify OSEK/VDX distributed application systems to discover subtle errors. Unfortunately, it faces a poor scalability for practical systems because the verification models derived from such systems are highly complex. This paper presents an efficient approach that addresses this problem by reducing the complexity of the verification model such that model checking can easily complete the verification.

Programming screencasts have two important applications in software engineering context: study developer behaviors, information needs and disseminate software engineering knowledge. Although programming screencasts are easy to produce, they are not easy to analyze or index due to the image nature of the data. Existing techniques extract only content from screencasts, but ignore workflow actions by which developers accomplish programming tasks. This significantly limits the effective use of programming screencasts in downstream applications. In this paper, we are the first to present a novel technique for recognizing workflow actions in programming screencasts. Our technique exploits image differencing and Convolutional Neural Network (CNN) to analyze the correspondence and change of consecutive frames, based on which nine classes of frequent developer actions can be recognized from programming screencasts. Using programming screencasts from Youtube, we evaluate different configurations of our CNN model and the performance of our technique for developer action recognition across developers, working environments and programming languages. Using screencasts of developers' real work, we demonstrate the usefulness of our technique in a practical application for actionaware extraction of key-code frames in developers' work.

Different objects have unique attributes, visual appearances and physical properties which help human visual system to recognize them better. But can object attributes help improve the object detection performance in computer vision? To answer this very question, we carry out extensive experimentation in this research work and claim that, indeed, object attributes improve the object detection performance significantly. We train feature pyramid networks to learn deep convolutional features for objects and their attributes. When used in combination with each other to infer bounding boxes and class scores for objects, these convolutional features show that object detection boosts significantly. We present a new method to boost the performance of object detection using object attributes in Detect-and-Describe (DaD) framework. We explain multiple approaches for boosting of object detection using their attributes. In these approaches, the convolutional features of attributes are merged with convolutional features of bounding box and class labels using different feature merging techniques to boost object detection. To report the performance of object detection boosting using DaD framework, we train our experimental models on aPascal train split and report performance on aPascal test split. Our results show that object attributes can help boost mean average precision (mAP) of object detection as significant as 2.68%.

Developers often look for solutions to programming problems in community Q&A sites like Stack Overflow. Due to the crowdsourcing nature of these Q&A sites, many user-provided answers are wrong, less optimal or out-of-date. Relying on community-curated quality indicators (e.g., accepted answer, answer vote) cannot reliably identify these answer problems. Such problematic answers are often criticized by other users. However, these critiques are not readily discoverable when reading the posts. In this paper, we consider the answers being criticized and their critique posts as controversial discussions in community Q&A sites. To help developers notice such controversial discussions and make more informed choices of appropriate solutions, we design an automatic open information extraction approach for systematically discovering and summarizing the controversies in Stack Overflow and exploiting official API documentation to assist the understanding of the discovered controversies. We apply our approach to millions of java/android-tagged Stack overflow questions and answers and discover a large scale of controversial discussions in Stack Overflow. Our manual evaluation confirms that the extracted controversy information is of high accuracy. A user study with 18 developers demonstrates the usefulness of our generated controversy summaries in helping developers avoid the controversial answers and choose more appropriate solutions to programming questions.

Summary To reduce heavy noise from degraded video in low or predictable latency and preserve privacy, a powerful and efficient video denoising algorithm is proposed based on fog computing for Visual Internet of Things. The conventional method is to remove noise in the cloud; however, this may overload computation and communication and raise security and privacy issues. The proposed denoising algorithm is distributed to heterogeneous devices at network edges to preserve privacy and avoid security risks as noise can be reduced in the fog rather than the cloud. To address the problems of latency, communication rate, and extremely heavy noise, structure registration, inter‐frame and inner‐frame filters, and distribution compensation are applied in the proposed algorithm. A scheme for encrypting the denoised data at network edges is provided so that security and privacy issues may be avoided during transmission and storage. Compared with other denoising approaches under extremely heavy noise conditions, the experimental results demonstrate that the proposed approach achieves superior denoising performance in terms of peak signal‐noise ratio and visual quality at low computational cost, high bandwidth efficiency, and low‐latency response in a fog computing manner.

This article studies synchronous online distributed software update, also known as rolling upgrade in DevOps, which in clouds upgrades software versions in virtual machine instances even when various failures may occur. The goal is to minimise completion time, availability degradation, and monetary cost for entire rolling upgrade by selecting proper parameters. For this goal, we propose a stochastic model and a novel optimisation method. We validate our approach to minimise the objectives through both experiments in Amazon Web Service (AWS) and simulations.

With the transformation of Internet of Things to Web of Things (WoT), a variety of applications are required to deal with huge volumes of real-time and heterogeneous data. However, in most applications, due to the weak semantics of data itself and the loose combination with specific scenarios, it is sometimes difficult to depict the spatiotemporal feature of the scenario in an application only through the data. In this paper, a spatiotemporal semantic scenario meta-model-based configurable platform is proposed for the development of WoT applications to address this issue, based on the data configuration, event stream configuration, and service encapsulation, the entire WoT scenario can be depicted with an abstract data model and related rules, and the business process can be changed by redefining corresponding rules when requirements change. A case study is given to verify the feasibility of our platform. The result shows that the platform can provide background support for WoT applications in a promising way.

To ensure the post quality, Q&A sites usually develop a list of quality assurance guidelines for "dos and don'ts", and adopt collaborative editing mechanism to fix quality violations. Quality guidelines are mostly high-level principles, and many tacit and context-sensitive aspects of the expected quality cannot be easily enforced by a set of explicit rules. Collaborative editing is a reactive mechanism after low-quality posts have been posted. Our study of collaborative editing data on Stack Overflow suggests that tacit and context-sensitive quality-assurance knowledge is manifested in the editing patterns of large numbers of collaborative edits. Inspired by this observation, we develop and evaluate a Convolutional Neural Network based approach to learn editing patterns from historical post edits for predicting the need of editing a post. Our approach provides a proactive policy assurance mechanism that warns users potential quality issues in a post before it is posted.

Summary OSEK/VDX, a development standard for automobiles, has now been widely adopted by automotive manufacturers for developing a vehicle‐mounted system. The ever increasing complexity of the system has created a challenge for ensuring the reliability of the developed OSEK/VDX applications in exhaustive way. Model checking as an exhaustive verification technique has attracted much attention in the automotive industry. To check OSEK/VDX applications by using model checking verification techniques, we have proposed a method based on SMT‐based bounded model checking. However, the method performs a poor efficiency in checking the OSEK/VDX applications that hold many loops, especially it is unable to deal with interruptions. In this paper, to apply model checking verification techniques to check a practical OSEK/VDX application, we develop and investigate an alterative approach based on the well‐known model checker Spin. In our Spin‐based approach, interruptions are taken into account, and moreover, 2 optimization strategies are used to boost the scalability and efficiency of the approach by reducing state space and accelerating bug detection. We have investigated the Spin‐based approach based on a series of experiments. The experimental results show that the approach is an impactful technique to verify the developed OSEK/VDX applications that hold a number of loops and interruptions.

With the wide spreading of mobile and Internet of Things (IoT) devices, music cognition as a meaningful task for music promotion has attracted a lot of attention around the world. How to automatically generate music score is an important part in music cognition, which acts as an important carrier so as to disposing huge quantity of music data in IoT networks or Internet. For the reason that the computers lack of the domain knowledge and cognitive ability, it is hard for computers to recognize the melody of music or write score while listening to the music. Therefore, a music cognition system is introduced to cognate music and automatically write score based on machine learning methods. First, considering large-scale data processing is needed by machine learning algorithms and a number of music devices are involved in the cognition system through Internet, fog computing is adopted in the proposed architecture to efficiently allocate computing resources. Then, the system can collect, preprocess, and store raw music data on the fringe nodes. Meanwhile, these data will be transmitted from fog nodes to cloud servers to form music databases. Then, machine learning algorithms, such as hidden Markov model and Gaussian mixture model, are performed in cloud servers to recognize music melody. Finally, a case study of music score generation demonstrates the proposed system. It is shown that the method provides an effective support to generate music score, and also proposed a promising way for the research and application of music cognition.

Rolling upgradeis a widely-used industry technique for updating software while a service provided by multiple instances of the software remains available. In cloud deployments of software, it is usual to implement the update step for rolling upgrade by replacing entire virtual machine instances. During the process of rolling upgrade, various failures may occur due to the complexity of software stack and the uncertainties of cloud platforms. Instance health checking and replacement are standard functionalities in most cloud infrastructures, though these create uncertainty in the duration of the whole upgrade procedure. In contrast, software and configuration errors are not usually detected by infrastructure functionalities, and if these happen, the entire rolling upgrade normally is unsuccessful and the system is left in an unsuitable state. In this paper, we propose an approach, named R2C, which innovates the stat of the art with our early error detection and predictability to increase the robustness of rolling upgrade on cloud platforms. We evaluate our techniques through real life testing in Amazon Web Service (AWS) and through a simulation.

One of the fundamental problem in data management and data integration fields is Record Matching, which refers to identifying records that relate to the same entities across different data sources. In recent literature, active learning has demonstrated to be effective for record matching. One of the key steps of active learning is to build a proper initial classifier, with which active learning algorithms can quickly locate informative examples for training accurate models. However, in this process, example labelling for model training is usually expensive. Even worse, if a weak initial classifier is used, the labelling cost can be significantly increased. In this paper, we propose an unsupervised algorithm to determine the initial classifier. The process of classifier initialization requires no labelling cost. Then on our proposed algorithm, we present an active sampling method for selecting informative examples. The experiments show that our approach achieves competitive learning performance with much less labelling cost than other approaches of active learning.

Summary Shop recommendation in large shopping malls is useful in the mobile internet era. With the maturity of indoor positioning technology, customers' indoor trajectories can be captured by radio frequency identification devices readers, which provides a new way to analyze customers' potential preferences. In this paper, we design three methods for the top‐N shop recommendation problem. The first method is an improved matrix factorization method fusing estimated prior customer preference matrix that is constructed by Session‐based Temporal Graph computing. The second method is a Bayesian personalized ranking method based on the first method. The third method is by tensor decomposition combined with Session‐based Temporal Graph. Besides, we exploit customer history radio frequency identification devices trajectory information to find customers' frequent paths and revise predicted rating values to improve recommendation accuracy. Our methods are effective in modeling customers' temporal dynamics. At the same time, our approach considers repeated recommendation of the same shop by designing rating update rules. The test dataset is formed byJoyCitycustomer behavior records.JoyCityis a large‐scale modern shopping center in downtown Shanghai, China. The results show that our approaches are effective and outperform previous state‐of‐the‐art approaches. Copyright © 2016 John Wiley & Sons, Ltd.

OSEK/VDX, a standard of automobile OS, has been widely adopted by many manufacturers to design and implement a vehicle-mounted OS. Currently, with increasing functionalities in vehicles, more and more complex applications are developed based on the OSEK/VDX OS. However, how to ensure the reliability of developed applications is becoming a challenge for developers. Based on our previous work, in this paper we present an efficient approach to verify the developed OSEK/VDX applications. In the presented approach, SMT-based bounded model checking technique is used to carry out verification in order to handle complex applications. Moreover, a series of optimization strategies are proposed and employed to improve the checking capability of our approach. We have implemented a tool according to the proposed approach and conducted many experiments. The experiment results show that our approach is capable of checking the safety property of large-scale OSEK/VDX applications. We also compared our approach with existing checking method, the comparison results indicate that our approach is an efficient and powerful technique in verifying OSEK/VDX applications.

Blocking is a technique of filtering unlikely matched pairs for record matching, which aims to collect all pairs of records that relate to the same entities across different data sources. Blocking has been broadly adopted in data mining and database. However, for big data, there is no fast and effective blocking algorithm yet, because the number of candidate pairs is tremendous between large data sets. In this paper, we report on a probabilistic parallelisation of a recently proposed blocking that is a sequential algorithm for efficient record matching in single machines. Our approach runs blocking processes distributedly on partitioned input data. In order to reduce data exchange among those blocking processes, we adopt a probabilistic technique to assure that the processes can run independently and meanwhile the aggregated result is correct with respect to common metrics. Our experimental analysis endorses the advantage of our technique and shows its novel scalability on a Hadoop MapReduce system deployed physically in a cloud.

Provenance is information about the origin and creation of data. In data science and engineering, such information is useful and sometimes even critical. In spite of that, provenance for big data is under-explored due to the challenges from the `Vs' of big data. In data analytics, users need to query history, reproduce intermediate or final results, tune models, and adjust parameters in runtime for making data-driven decisions. In addition, users need to evaluate data and pipeline trustworthiness. Towards realising these functionalities for big data provenance, we propose a solution, called LogProv, which needs to renovate data pipelines or even some of big data software infrastructure to generate structured logs for pipeline events, and then stores data and logs separately. The data are explicitly linked to the logs, which implicitly record pipeline semantics. Semantic information can be retrieved from the logs easily since the logs are well defined and structured beforehand. We implemented LogProv in Apache Pig, and adopted ElasticSearch to provide query service. In this paper LogProv is evaluated in a Hadoop ecosystem hosted by a cloud and empirically case-studied. The results show that LogProv is efficient since the performance overhead is no more than 10%, the query can be responded within 1 second, the trustworthiness is marked clearly, and there is no impact on the data processing logic of original pipelines.

Concurrency semantics plays an important role in both concurrency theory and software engineering. Although many results on various concurrency semantics have been proposed, there is still room for improvement. This paper focuses on the locality semantics, an important non-interleaving semantics, based on studying the relationship between the located CCS and the π-calculus. We present a practical full abstraction result for the locality semantics, and reduce the location bisimulation of the located CCS to the observation bisimulation of the π-calculus. The full abstraction result respects process finiteness, i.e., finite processes of the located CCS are mapped onto finite π-processes. As a result, the location bisimulation on finite processes of the located CCS can be proved by an existing proof system on finite π-processes, which is not achieved in [31].

Exchange protocols are an important theoretic basis to make secure electronic commerce and electronic business transactions possible, in which the fairness is a crucial property. To ensure and verify the property, a specific model is proposed, based on the extensive game with imperfect information. Fairness is built in the protocol game and the corresponding game tree. To verify the property, a tree analysis method is offered, and a linear time algorithm is given. As a case study, some flaws of ASW protocol are found.

Interrupts are important aspects of real-time embedded systems to handle events in time. When there exist nested interrupts in a real-time system, and an urgent interrupt is allowed to preempt the current interrupt handling, the design and analysis of the system become difficult due to the lack of appropriate behavioral models. This paper proposes a compositional model for nested interrupts and an analysis named environmental simulation. We present a new kind of timed transition system, named controller automata, to treat interrupts. Together with an interrupt environment modeled as a timed automaton, and a scheduler as a timed automaton with semaphores, the system behaviors with nested interrupts are realized by a sequence of transitions with time. Although various verification problems for this model are undecidable in general, it is shown that the reachability of error states is practically solvable with our implementation of the environmental simulation by Maude.

The spi calculus has been proved useful for reasoning about security protocols. It is however difficult to mechanize the equivalence checking in that framework due to the complexity caused by name passing communications. The paper proposes a calculus for the analysis of the security protocols (SPC for short) as a simplification of the spi calculus. SPC can explicitly express environment knowledge, protocol participants and their knowledge. We present its syntax and semantics, and specify some security properties in terms of equivalence relations. Finally two examples of formal verification is given.