Abstract Static analysis plays a crucial role in program optimization, bug detection, and automated testing. Dyck-reachability provides a foundational formulation for static analysis, as Dyck grammars can model critical properties such as field and context sensitivity, thus offering broad applicability. This paper shows that static analysis problems modeled as Dyck-reachability on bidirected graphs can be encoded into the EUF SMT theory; consequently, all such problems admit efficient formulation and solution via EUF-based SMT solvers. By leveraging the optimized nature of modern SMT solvers, our method achieves efficiency comparable to state-of-the-art graph-based bidirected Dyck-reachability algorithms while eliminating the need for developing complex specialized graph reachability algorithms. Our approach opens new avenues for solving these classical static analysis problems, demonstrating the strong potential of SMT solvers in encoding static analysis solutions.

Abstract The principled combination of symbolic execution and random testing lacks a formal foundation, especially in deciding which inputs to symbolize. We propose selective concolic testing, a cost-aware framework that formulates this choice as an optimized policy problem of a MDP (Markov Decision Process). We model program exploration over a finite control-flow graph, where MDP states represent covered statements, actions partition path constraints into symbolic and random fragments, rewards reflect coverage gain, and costs account for SMT solving effort and sampling inefficiency. Our framework yields the first formal characterization of selective symbolization as policy synthesis in a probabilistic system. We prove that exact policy computation is intractable due to the exponential state space and the hardness of solution-density estimation via model counting. Our formulation enables a practical approximation: we partition constraint dependency graphs and use machine learning to predict solver timeouts, guiding per-constraint symbolization decisions. Built on top of KLEE and JFS, our prototype validates the approach on real-world floating-point benchmarks. Results show that selectively symbolizing inputs, guided by predicted solvability and cost, significantly improves coverage efficiency. Our work thus provides both a rigorous theoretical foundation and a practical instantiation for hybrid program analysis.

The development of formal methods (FM) in China dates back to the early 1950s, when several logicians shifted their research focus from mathematics to theoretical computer science and began advocating the application of mathematical logic to enhance the rigor of computing systems. A significant expansion of FM in China emerged in the 1980s, pioneered by a new generation of talented computer scientists who had visited, studied, and/or worked in Western countries, such as the United Kingdom and the United States, closely tied to China’s reform and opening-up policy. A notable milestone was the establishment of the United Nations University International Institute for Software Technology (UNU/IIST) in Macau in the early 1990s, which played a crucial role in advancing FM research and collaboration in China. In recent years, the return of an increasing number of talented young scholars has further strengthened China’s FM community, elevating its influence and contribution within the global FM landscape.

Recent advances in foundation models have motivated hybrid programming that integrates natural language descriptions, formal specifications, and executable code. A critical challenge in such systems lies in achieving semantic alignment across heterogeneous representations at different abstraction levels. This challenge is particularly pressing in programmatic reinforcement learning (PRL) for robotics, where long-horizon, sparse-reward tasks demand tight coordination between symbolic reasoning and continuous control. Existing approaches either rely on manually engineered symbolic representations or on LLM-generated plans that might be untrustworthy or infeasible to execute, leaving such fundamental gaps unaddressed. We present a closed-loop, counterexample-guided synthesis framework that unifies LLM-based planning, formal verification, and differentiable behavior tree (BT) synthesis for neuro-symbolic policy learning. The framework first converts natural language task descriptions into PDDL, then generates valid high-level plans via a Guess-Check-Critique loop that interleaves LLM generation with SMT-based verification. We automatically compile symbolic abstractions in verified plans into parameterized termination conditions, and co-optimize them with low-level policies to enforce semantic consistency. The learned sub-policies are composed into an integrated BT and fine‑tuned to ensure task-level executability. Furthermore, we perform closed-loop iterations of abstractions and compilations using feedback from verification and learning, while incrementally building a reusable skill library for efficient knowledge transfer. Experiments on challenging long-horizon robotic tasks show that our method exceeds state-of-the-art methods while providing interpretability and generalization.

Symbolic execution faces the challenge of generating valid inputs when analyzing the program with complex input formats. Token-based symbolic execution can partially tackle this challenge but is still doomed by the difficulty of passing input checking and failing to analyze the code after input checking. We propose Lase , an online input grammar synthesis aided symbolic execution method, to generate valid inputs for improving the effectiveness of symbolic execution. Inside Lase , we propose an input grammar-oriented search strategy and a token-level grammar synthesis method. The search strategy selects the paths to cover more syntax rules in priority. The token-level grammar synthesis improves the synthesized grammar’s precision and completeness while ensuring efficiency. The experimental results on real-world parsing programs with complex input grammars demonstrate that Lase can improve the coverage of parsing code and generate more valid inputs to improve the coverage of functionality code significantly. Furthermore, compared with the state-of-the-art grammar synthesis methods, the grammars learned by Lase have better precision and recall on most benchmark programs.

Multi-robot task planning and collaboration are critical challenges in robotics. While Behavior Trees (BTs) have been established as a popular control architecture and are plannable for a single robot, the development of effective multi-robot BT planning algorithms remains challenging due to the complexity of coordinating diverse action spaces. We propose the Multi-Robot Behavior Tree Planning (MRBTP) algorithm, with theoretical guarantees of both soundness and completeness. MRBTP features cross-tree expansion to coordinate heterogeneous actions across different BTs to achieve the team's goal. For homogeneous actions, we retain backup structures among BTs to ensure robustness and prevent redundant execution through intention sharing. While MRBTP is capable of generating BTs for both homogeneous and heterogeneous robot teams, its efficiency can be further improved. We then propose an optional plugin for MRBTP when Large Language Models (LLMs) are available to reason goal-related actions for each robot. These relevant actions can be pre-planned to form long-horizon subtrees, significantly enhancing the planning speed and collaboration efficiency of MRBTP. We evaluate our algorithm in warehouse management and everyday service scenarios. Results demonstrate MRBTP's robustness and execution efficiency under varying settings, as well as the ability of the pre-trained LLM to generate effective task-specific subtrees for MRBTP.

Recently, substantial progress has been achieved in leveraging deep learning models for tabular data learning. However, despite significant advancements, the predominant focus of these endeavors has been on augmenting the performance of contemporary deep learning models. Consequently, the interpretability of such models is frequently overlooked or rendered secondary, thereby posing a challenge in comprehending their underlying decision-making processes. In this work, we propose a novel HyperNetwork Slide Decision Tree (HyperSDT) approach to achieve interpretable deep learning for tabular data while maintaining a comparable accuracy to state-of-the-art methods. HyperSDT provides a comprehensive interpretable framework with interpretability by using Silde Decision Tree and Decision Transformer together. Our experimental results demonstrate that our framework is competitive with prior baselines under various tabular learning benchmarks while providing better interpretability. The code can be achieved via https://github.com/hunan-create/HyperSDT.

By characterizing interactions and influences across individuals, networked interference aims to estimate cross-individual treatment effects. For each individual, one of the central components of existing approaches is to manually design an exposure mapping from their neighboring covariates (including their own ones) to different exposure conditions. However, handcraft neighboring structures defined by such manual schemes struggle to capture the complex and flexible structures exhibited by real-world social networks. To bridge this gap, we propose an Automated Exposure Mapping Network (AEMNet) by capturing networked interference conditions automatically with Graph Neural Networks (GNNs) and achieving mapping with deep embedded clustering. The learned representations between individuals in the graph structure reveal patterns and structures hidden behind data, facilitating application on large-scale, relationally complex networked data. We conducted extensive experiments demonstrating that our approach outperforms the baselines in both quality and flexibility, underscoring its ability to better characterize the interference relationships.

Large Vision-Language models (LVLMs) have demonstrated remarkable performance in a wide range of vision-language tasks as an efficient input/output system. However, the lack of adversarial robustness at the input side and the widespread hallucination phenomenon at the output side significantly undermine user trust in them. Current solutions to the former tend to sacrifice the general performance of LVLMs, while solving the latter requires a large amount of engineering costs. To address these challenges, we propose a two-stage optimization strategy called RCDT (Robust CLIP-guided Deep Thinking), which aims to enhance the adversarial robustness of LVLMs with minimal general performance loss while reducing hallucinations. First, we introduce a constrained adversarial fine-tuning approach for CLIP to limit the general performance loss during the enhancement of robustness. Furthermore, this CLIP is used to think deeply about the output process of LVLMs to reduce hallucinations. Experiments show that RCDT not only reduce general performance loss by more than half while maintaining adversarial robustness compared to the baselines, but also demonstrate good performance in mitigating hallucinations.

In this paper, we aim to tackle the challenging Black-Box Open-Set Domain Adaptation (BB-OSDA) task. BB-OSDA enables conducting Open-Set Domain Adaptation (OSDA) with solely a black-box source model, broadening the application scope of OSDA. Inspired by the significant success of pre-trained large vision-language (ViL) models in various applications, we propose a novel method, termed Knowledge Aggregation for Black-box Open-set domain adaptatioN (KABON), which leverages the power of ViL models to solve the BB-OSDA problem. Specifically, we first devise a novel knowledge aggregation approach to harness both the generic knowledge from the ViL model and the task-specific knowledge from the black-box source model. Subsequently, we utilize a Gaussian Mixture Model (GMM) with entropy criterion to divide samples of target domain into shared or novel classes. Furthermore, a self-correction strategy is proposed to refine the division of shared and novel classes. Finally, we leverage the divided samples through entropy minmax learning to simultaneously achieve shared classes adaptation and novel classes detection. Experiments conducted on multiple benchmark datasets demonstrate the effectiveness of our proposed method.

Behavior Trees (BTs) are increasingly becoming a popular control structure in robotics due to their modularity, reactivity, and robustness. In terms of BT generation methods, BT planning shows promise for generating reliable BTs. However, the scalability of BT planning is often constrained by prolonged planning times in complex scenarios, largely due to a lack of domain knowledge. In contrast, pre-trained Large Language Models (LLMs) have demonstrated task reasoning capabilities across various domains, though the correctness and safety of their planning remain uncertain. This paper proposes integrating BT planning with LLM reasoning, introducing Heuristic Behavior Tree Planning (HBTP)-a reliable and efficient framework for BT generation. The key idea in HBTP is to leverage LLMs for task-specific reasoning to generate a heuristic path, which BT planning can then follow to expand efficiently. We first introduce the heuristic BT expansion process, along with two heuristic variants designed for optimal planning and satisficing planning, respectively. Then, we propose methods to address the inaccuracies of LLM reasoning, including action space pruning and reflective feedback, to further enhance both reasoning accuracy and planning efficiency. Experiments demonstrate the theoretical bounds of HBTP, and results from four datasets confirm its practical effectiveness in everyday service robot applications.

Behavior Trees (BTs), originated from the control of Non-Player-Characters (NPCs), have been widely embraced in robotics and software engineering communities due to their modularity, reactivity, and other beneficial characteristics. It is highly desirable to synthesize BTs automatically. The consequent challenges are to ensure the generated BTs semantically correct, well-structured, and efficiently executable. To address these challenges, in this paper, we present a novel reactive synthesis method for BTs, namely EffBT, to generate correct and efficient controllers from formal specifications in GR(1) automatically. The idea is to construct BTs soundly from the intermediate strategies derived during the algorithm of GR(1) realizability check. Additionally, we introduce pruning strategies and use of Parallel nodes to improve BT execution, while none of the priors explored before. We prove the soundness of the EffBT method, and the experimental results demonstrate its effectiveness in various scenarios and datasets.

Behavior Trees (BTs) are a widely used control architecture in robotics, renowned for their robustness and safety, which are especially crucial for everyday service robots. Recently, several methods have been proposed to automatically plan BTs to accomplish specific tasks. However, existing research in BT planning lacks two main aspects: (1) the absence of a standard platform for modeling and planning BTs, along with testing benchmarks; and (2) insufficient metrics for a comprehensive evaluation of BT planning algorithms. In this paper, we propose Behavior Tree Planning Gym (BTPG), the first platform and benchmark for BT planning in everyday service robots. In BTPG, behavior nodes are represented by predicate logic, and objects are categorized to better define the predicate domains and action models. The BT planning problem is then formulated in the STRIPS style. We support four environments and three simulators with different action models, which cover most of the needs of everyday service activities. We design a dataset generator for each environment and test three state-of-the-art BT planning algorithms, as well as one proposed by us, using various common metrics. In addition, we design three advanced metrics, planning progress, region distance, and execution robustness, to gain deeper insights into these BT planning algorithms. With a standard test benchmark, we hope BTPG can inspire and accelerate progress in the field of BT planning. Our codes are available at https://github.com/DIDS-EI/BTPG.

Recently, formal verification of deep neural networks (DNNs) has garnered considerable attention, and over-approximation based methods have become popular due to their effectiveness and efficiency. However, these strategies face challenges in addressing the "unknown dilemma" concerning whether the exact output region or the introduced approximation error violates the property in question. To address this, this paper introduces theUR4NNVverification framework, which utilizes under-approximation reachability analysis for DNN verification for the first timeUR4NNV focuses on DNNs with Rectified Linear Unit (ReLU) activations and employs a binary tree branch-based under-approximation algorithm. In each epoch, UR4NNVunder-approximates a sub-polytope of the reachable set and verifies this polytope against the given property. Through a trial-and-error approach,UR4NNVeffectively falsifies DNN properties while providing confidence levels when reaching verification epoch bounds and failing falsifying properties. Experimental comparisons with existing verification methods demonstrate the effectiveness and efficiency ofUR4NNVsignificantly reducing the impact of the "unknown dilemma".

Floating-point exceptions are hard to avoid and can cause disastrous consequences. However, testing methods for floating-point exceptions in GPU programs are currently quite limited due to their closed-source nature. Existing tools, even the state-of-the-art Xscope, still exhibit low search efficiency and poor input coverage. In this paper, we combine interval-wise random sampling and Markov Chain Monte Carlo (MCMC) sampling in a synergistic way to efficiently detect exception-inducing inputs in GPU programs. To improve the search efficiency, based on the bit patterns of exceptional floating-point values, we propose a floating-point format-aware input space partitioning method for random sampling and define a unified fitness function for MCMC sampling. We implement our approach in a tool DFEG and demonstrate it on 76 functions from the CUDA Math Library, HPC programs, and FPBench. DFEG outperforms Xscope in terms of both effectiveness and efficiency. DFEG finds$949 \times$more exceptions than Xscope and detects new exceptions in 9 functions where Xscope fails. Moreover, compared to Xscope, DFEG achieves an average$34 \times$speedup.

Abstract is a C program verifier that synergizes symbolic execution and abstract interpretation. This year, v2.0 introduces a loop transformation scheme based on recurrence analysis to handle programs involving nonlinear arithmetic. By combining loop transformations, v2.0 achieved a score of 1031 and won first place in the ReachSafety-Loops category, demonstrating the effectiveness of the methods employed in v2.0.

Few-shot learning (FSL) aims to enable learning models with the ability to automatically adapt to novel (unseen) domains in open-world scenarios. Nonetheless, there exists a significant disparity between the vast number of new concepts encountered in the open world and the restricted available scale of existing FSL works, which primarily focus on a limited number of novel classes. Such a gap hinders the practical applicability of FSL in realistic scenarios. To bridge this gap, we propose a new problem named Few-Shot Learning with Many Novel Classes (FSL-MNC) by substantially enlarging the number of novel classes, exceeding the count in the traditional FSL setup by over 500-fold. This new problem exhibits two major challenges, including the increased computation overhead during meta-training and the degraded classification performance by the large number of classes during meta-testing. To overcome these challenges, we propose a Simple Hierarchy Pipeline (SHA-Pipeline). Due to the inefficiency of traditional protocols of EML, we re-design a lightweight training strategy to reduce the overhead brought by much more novel classes. To capture discriminative semantics across numerous novel classes, we effectively reconstruct and leverage the class hierarchy information during meta-testing. Experiments show that the proposed SHA-Pipeline significantly outperforms not only the ProtoNet baseline but also the state-of-the-art alternatives across different numbers of novel classes.

Neural network verification, particularly verification of robustness properties, has received much research attention. However, many existing verification methods overlook the influence of floating-point rounding errors in the deployed neural networks, resulting in unsound verification outcomes. In this paper, we propose a sound robustness verification approach aiming at overcoming this limitation. Our method utilizes real-number intervals to approximate floating-point arithmetic and abstracts floating-point neural networks into equivalent networks using real-number interval arithmetic semantics, thereby effectively taking into account for floating-point rounding errors. We sub-sequently employ exact MILP formulations to verify robustness over these abstracted networks. We introduce FMIPVerify, a dedicated verification tool tailored to ensure the soundness of floating-point neural network verification. Experimental results demonstrate that FMIPVerify significantly improves the robustness verification ability in floating-point ReLU neural networks compared to established complete methods like MIPVerify.

Abstract serves as an automatic test generation tool designed for C programs based on symbolic execution. employs fuzzing-based pre-analysis and combines static symbolic execution and dynamic symbolic execution to improve the effectiveness of test generation. achieves 5132 scores and is ranked 4th in the branch coverage track of Test-Comp 2024.

Standing out as one of the most widely used tools in Cross-Domain Few-Shot Learning (CDFSL), data augmentation forms the bedrock of numerous recent advancements. However, the current augmentations in CDFSL are limited in their ability to modify high-level semantic attributes, resulting in a lack of diversity along key semantic dimensions. One of the most promising tools to edit images with key semantic attributes, e.g. backgrounds, is image-to-image generation via large multimodal models (LMMs). Given the promising image editing results of recent LMMs, we delve into leveraging LMMs to augment data diversity for CDFSL. We propose a novel method named, Multimodal Few-shot Image Editing (MFIE), which uses LMMs to automatically translate class-specific images into class-agnostic natural language descriptions for various key semantic attributes in target domains and editing origin images based on class-agnostic natural language descriptions. To filter out corrupted data that disturbs the class-specific information, we apply semantic filtering using image-language similarity. Experiments on Meta-Datset show that MFIE surpasses SOTA CDFSL algorithms.

There has been emerging researches on leveraging large language models (LLMs) to improve the automation of theorem proving. However, they are still suffering from low accuracy and efficiency. In this paper, we propose to strengthen the existing approach by enhancing a language agent, which provides automatic explanation of terms and repair of tactics parameters. Term explanation explains terms specific to the proof obligations formally and tactic parameter repair complements the potentially correct proof tactics as much as possible. Similar to the existing approach, the agent uses GPT-4 as query objects in a search policy. During the search, we add term explanation to the prompt, and then the policy selects a proof tactic and repairs it. The repaired tactics interact with the theorem prover (Coq), and the execution result is fed back to build the prompt for the next policy invocation. We evaluate our approach on subsets of the CompCert project implemented using Coq. Our approach proves 8.11% more theorems than the existing language agent COPRA, and demonstrates faster search and proof speed. Besides, when term explanation and tactic parameter repair are applied, the performance of the SOTA method PROVERBOT9001 can be also improved.

Deep neural network (DNN) has been increasingly deployed as a key component in safety-critical systems. However, the credibility of DNN components is uncertain due to the absence of formal specifications for their data preconditions, which are essential for ensuring trustworthy postconditions.In this paper, we propose a guess-and-check-based framework PreBoxes to automatically synthesize Boxes sufficient preconditions for DNN concerning rich safety and robustness postconditions.The framework operates in two phases: the guess phase generates potentially complex candidate preconditions through heuristic methods, while the check phase verifies these candidates with formal guarantees.The entire framework supports automatic and adaptive iterative running to obtain weaker preconditions as well.Such resulting preconditions can be leveraged to shield DNN for safety and enhance the interpretability of DNN in application.PreBoxes has been evaluated on over 20 models with 23 trustworthy properties of 4 benchmarks and compared with 3 existing typical schemes.The results show that not only does PreBoxes generally infer weaker non-trivial sufficient preconditions for DNN than others, but also it expands competitive capabilities to handle both complex properties and Non-ReLU complex structured networks.

Regression Testing Selection (RTS) reduces the cost of regression testing by only running test cases affected by code changes. Due to the bottleneck of single granularity analyses, the latest RTS techniques tend to analyze with mixed granularities. However, a better synergy of the existing RTS techniques is still challenging. Besides, we have found that once existing RTS approaches use static method-level analysis, handling external library callbacks is difficult, leading to the missed selection of affected test cases.

Floating-point arithmetic is notorious for its rounding errors, which can propagate and accumulate, leading to unacceptable results. Detecting inputs that can trigger significant floating-point errors is crucial for enhancing the reliability of numerical programs. Existing methods for generating error-triggering inputs often rely on costly shadow executions that involve high-precision computations or suffer from false positives. This paper introduces chain conditions to capture the propagation and accumulation of floating-point errors, using them to guide the search for error-triggering inputs. We have implemented a tool named FPCC and evaluated it on 88 functions from the GNU Scientific Library, as well as 21 functions with multiple inputs from previous research. The experimental results demonstrate the effectiveness and efficiency of our approach: (1) FPCC achieves 100% accuracy in detecting significant errors for the reported rank-1 inputs, while 72.69% rank-1 inputs from the state-of-the-art tool ATOMU can trigger significant errors. Overall, 99.64% (1049/1053) of the inputs reported by FPCC can trigger significant errors, whereas only 19.45% (141/723) of the inputs reported by ATOMU can trigger significant errors; (2) FPCC exhibits a 2.17x speedup over ATOMU in detecting significant errors; (3) FPCC also excels in supporting functions with multiple inputs, outperforming the state-of-the-art technique. To facilitate further research in the community, we have made FPCC available on GitHub at https://github.com/DataReportRe/FPCC .

Message-passing programs involve several processes with channel-based communications to deal with tasks concurrently. The complex computations and communications between processes make the verification of message-passing programs hard. By regarding the functions in programs as uninterpreted functions, we focus on the verification problem of message-passing uninterpreted programs. Although the usage of uninterpreted functions alleviates the computational difficulties brought by functions, the verification problem is still undecidable in general. In this work, we provide a decidable subclass of message-passing uninterpreted programs, wherein programs in this subclass satisfy the property of k-record coherence . The decidability result closely relies on communicating finite-state machine (CFM) with bounded channels. Based on the decidability result, we proposed a verification framework for message-passing uninterpreted programs.

Summary Constraint solving is the enabling technique for symbolic execution. The advancement of constraint solving boosts the development and application of symbolic execution. Modern Satisfiability Modulo Theories (SMT) solvers provide the mechanism of solving strategy, allowing users to control the solving procedure. This mechanism significantly improves the solver's generalization ability. We observe that the symbolic executions of different programs are different constraint solving problems. Therefore, we propose synthesizing solving strategies for a program to fit the program's symbolic execution best. To achieve this, we propose an adaptive framework for synthesizing solving strategies, in which the constraints are classified into different categories, and the solving strategies are synthesized for different categories on demand. We propose novel synthesis algorithms that combine the offline trained deep learning models and online tuning to synthesize the solving strategy. The algorithms balance the synthesis overhead and the improvement achieved by the synthesized solving strategy. We have implemented our method on the state‐of‐the‐art symbolic execution engine KLEE for C programs and Symbolic Pathfinder (SPF) for Java programs. The results of the extensive experiments indicate that our method effectively improves the efficiency of symbolic execution. For the Coreutils benchmark, our method, on average, increases the numbers of paths and queries by 74.37% and 73.94% under Breadth First Search (BFS), respectively. Besides, we applied our method to a different benchmark of C programs and a benchmark of Java programs to validate the generalization ability. The results demonstrate that for the C benchmark, our method increases the numbers of paths and queries by 71.09% and 70.60% under BFS, respectively; For the Java benchmark, our method increases the numbers of paths and queries by 50.31% and 49.93% under BFS, respectively. These results show that our method has a good generalization ability.

Recent research has revealed that deep generative models including flow-based models and Variational Autoencoders may assign higher likelihoods to out-of-distribution (OOD) data than in-distribution (ID) data. However, we cannot sample OOD data from the model. This counterintuitive phenomenon has not been satisfactorily explained and brings obstacles to OOD detection with flow-based models. In this article, we prove theorems to investigate the Kullback-Leibler divergence in flow-based model and give two explanations for the above phenomenon. Based on our theoretical analysis, we propose a new method KLODS to leverage KL divergence and local pixel dependence of representations to perform anomaly detection. Experimental results on prevalent benchmarks demonstrate the effectiveness and robustness of our method. For group anomaly detection, our method achieves 98.1% AUROC on average with a small batch size of 5. On the contrary, the baseline typicality test-based method only achieves 64.6% AUROC on average due to its failure on challenging problems. Our method also outperforms the state-of-the-art method by 9.1% AUROC. For point-wise anomaly detection, our method achieves 90.7% AUROC on average and outperforms the baseline by 5.2% AUROC. Besides, our method has the least notable failures and is the most robust one.

Uninterpreted predicate solving is a fundamental problem in formal verification, including loop invariant and constrained horn clauses predicate solving. Existing approaches have been mostly in symbolic ways. While achieving sustainable progress, they still suffer from inefficiency and seem unable to leverage the ever-increasing computility, such as GPU. Recently, neural relaxation has been proposed to tackle this problem. They treat the uninterpreted predicate-solving task as an optimization problem by relaxing the discrete search process into a learning process of neural networks. However, two bottlenecks keep them from being valid. First, relaxed neural networks cannot match the original semantics of predicates rigorously; second, the neural networks are difficult to train to reach global optimization. Therefore, this article presents a novel discrete neural architecture with the Abstract Gradient Decent (AGD) algorithm to directly solve uninterpreted predicates in the discrete hypothesis space. The abstract gradient is for discrete neurons whose calculation rules are designed in an abstract domain. Our approach conforms to the original semantics of predicates, and the proposed AGD algorithm can achieve global optimization satisfactorily. We implement the tool Dasp in the Boxes abstract domain to solve uninterpreted predicates in the QF-NIA SMT theory. In the experiments, Dasp has outperformed seven state-of-the-art tools across three predicate synthesis tasks.

Constraint solving stands out as a significant bot-tleneck in symbolic execution. Caching is a commonly adopted approach to alleviate this bottleneck. However, the cutting-edge caching technique targeting unsatisfiable constraints, known as unsatisfiable core caching, primarily involves checking whether the constraint being solved contains an unsatisfiable core that has been previously collected. Such straightforward reuse frequently proves less effective in numerous scenarios. In this paper, we present a novel method to enhance the utilization of unsatisfiable cores. By excavating unsatisfiable cores, our method can compute an easily solvable over-approximation that tends to be unsatis-fiable for each constraint, which facilitates the determination of the satisfiability of the original constraint. We implemented our method on KLEE symbolic executor. The evaluation results on 27 real-world programs are encouraging.

Inferring loop invariants is one of the most challenging problems in program verification. It is highly desired to incorporate machine learning when inferring. This paper presents a Reinforcement Learning (RL) pruning framework to infer loop invariants over a general nonlinear hypothesis space. The key idea is to synergize the RL-based pruning and SMT solving to generate candidate invariants efficiently. To address the sparse reward problem in learning, we design a novel two-dimensional reward mechanism that enables the RL pruner to recognize the capability boundary of SMT solvers and learn the pruning heuristics in a few rounds. We have implemented our approach with Z3 SMT solver in the tool called LIPuS and conducted extensive experiments over the linear and nonlinear benchmarks. Experiment results show that LIPuS can solve the most cases compared to the state-of-the-art loop invariant inference tools such as Code2Inv, ICE-DT, GSpacer, SymInfer, ImplCheck, and Eldarica. Especially, LIPuS outperforms them significantly on nonlinear benchmarks.

Fuzzy logic is widely applied in various applications. However, verifying the correctness of fuzzy logic models can be difficult. This extended abstract presents our ongoing work on verifying fuzzy logic models. We treat a fuzzy logic model as a program and propose a verification method based on symbolic execution for fuzzy logic models. We have developed and implemented the environment models for the common functions and the inference rules in fuzzy logic models. Our preliminary evaluation shows the potential of our verification method.

Kullback-Leibler (KL) divergence is one of the most important measures to calculate the difference between probability distributions. In this paper, we theoretically study several properties of KL divergence between multivariate Gaussian distributions. Firstly, for any two $n$-dimensional Gaussian distributions $\mathcal{N}_1$ and $\mathcal{N}_2$, we prove that when $KL(\mathcal{N}_2||\mathcal{N}_1)\leq \varepsilon\ (\varepsilon>0)$ the supremum of $KL(\mathcal{N}_1||\mathcal{N}_2)$ is $(1/2)\left((-W_{0}(-e^{-(1+2\varepsilon)}))^{-1}+\log(-W_{0}(-e^{-(1+2\varepsilon)})) -1 \right)$, where $W_0$ is the principal branch of Lambert $W$ function. For small $\varepsilon$, the supremum is $\varepsilon + 2\varepsilon^{1.5} + O(\varepsilon^2)$. This quantifies the approximate symmetry of small KL divergence between Gaussian distributions. We further derive the infimum of $KL(\mathcal{N}_1||\mathcal{N}_2)$ when $KL(\mathcal{N}_2||\mathcal{N}_1)\geq M\ (M>0)$. We give the conditions when the supremum and infimum can be attained. Secondly, for any three $n$-dimensional Gaussian distributions $\mathcal{N}_1$, $\mathcal{N}_2$, and $\mathcal{N}_3$, we theoretically show that an upper bound of $KL(\mathcal{N}_1||\mathcal{N}_3)$ is $3\varepsilon_1+3\varepsilon_2+2\sqrt{\varepsilon_1\varepsilon_2}+o(\varepsilon_1)+o(\varepsilon_2)$ when $KL(\mathcal{N}_1||\mathcal{N}_2)\leq \varepsilon_1$ and $KL(\mathcal{N}_2||\mathcal{N}_3)\leq \varepsilon_2$ ($\varepsilon_1,\varepsilon_2\ge 0$). This reveals that KL divergence between Gaussian distributions follows a relaxed triangle inequality. Note that, all these bounds in the theorems presented in this work are independent of the dimension $n$. Finally, we discuss several applications of our theories in deep learning, reinforcement learning, and sample complexity research.

Robustness of deep neural networks (DNNs) has caused great concerns in the academic and industrial communities, especially in safety-critical domains. Instead of verifying whether the robustness property holds or not in certain neural networks, this paper focuses on training robust neural networks with respect to given perturbations. State-of-the-art training methods, interval bound propagation (IBP) and CROWN-IBP, perform well with respect to small perturbations, but their performance declines significantly in large perturbation cases, which is termed “drawdown risk” in this paper. Specifically, drawdown risk refers to the phenomenon that IBP-family training methods cannot provide expected robust neural networks in larger perturbation cases, as in smaller perturbation cases. To alleviate the unexpected drawdown risk, we propose a global and monotonically decreasing robustness training strategy that takes multiple perturbations into account during each training epoch (global robustness training), and the corresponding robustness losses are combined with monotonically decreasing weights (monotonically decreasing robustness training). With experimental demonstrations, our presented strategy maintains performance on small perturbations and the drawdown risk on large perturbations is alleviated to a great extent. It is also noteworthy that our training method achieves higher model accuracy than the original training methods, which means that our presented training strategy gives more balanced consideration to robustness and accuracy.

It is difficult to write a numerical program that does not incur floating-point exceptions in practice. To detect floatingpoint exceptions, most existing methods use static analysis, which may induce false alarms (due to over-approximation), or suffer from scalability issues (since solving floating-point constraints is expensive). Fuzzing is a widely used technique to finding bugs, but existing fuzzing techniques have not yet considered the specific format of floating-point and are lack of guidance for detecting floating-point exceptions. In this paper, we propose a floating-point format aware coverage-based grey-box fuzzing to detect floating-point exceptions for numerical programs. More specifically, we propose a novel mutation strategy for floating-point format aiming at producing valid floating-point test inputs. Moreover, we present a new guidance aiming to search for test inputs that are closer to exposing exceptions. We implement our approach as a tool, named NumFUZZ, based on AFL. We have conducted experiments to evaluate NUMFUZZ on GNU Scientific Library (GSL) and Sun’s C math library respectively. The preliminary experimental results suggest that our approach has promising ability in detecting floating-point exceptions and achieving high floating-point branch coverage in real-world numerical programs.

Constraint solving and environment modeling are two challenging problems for symbolic execution. When a program contains non-linear expressions, it is difficult for symbolic execution to explore the program’s whole path space due to the high complexity of the constraint solving for the nonlinear constraints. Besides, when the program uses a third-party library and the source code of the library is not available, the symbolic execution of the program often under-approximates the analysis by concrete execution or over-approximates by introducing new symbolic variables, which may fail to explore the whole path space or introduce false alarms, respectively. This paper proposes FUSE, a framework of synergizing symbolic execution and fuzzing by function-level selective symbolization to tackle these problems. First, FUSE collects the path constraints of each function selectively and introduces symbolic function invocation expressions for the complex or third-party functions. Then, FUSE combines SMT solving and fuzzing to solve the path constraints. We have implemented FUSE on the start-of-theart symbolic execution engine KLEE. The experimental results demonstrate that FUSE effectively and efficiently improves the code coverage. Compared with the state-of-the-art, FUSE achieves 6. 6x speedups for achieving the same code coverage.

Abstract Worst-case resource usage provides a useful guidance in the design, configuration and deployment of software, especially when it runs under a context with limited amount of resources. Static resource-bound analysis can provide sound upper bounds of worst-case resource usage but may provide too conservative, even unbounded, results. In this paper, we present a resource-usage-aware fuzzing approach to estimate worst-case resource usage. The key idea is to guide the fuzzing process using resource-usage amount together with resource-usage relevant coverage. Moreover, we leverage semantic patch to make use of static analysis information (including control-flow, function-call, etc.) to instrument the original program, for the sake of aiding the subsequent fuzzing. We have conducted experiments to estimate worst-case resource usage of various resources in real-world programs, including heap memory, stack depths, sockets, user-defined resources, etc. The preliminary experimental results show the promising ability of our approach in estimating worst-case resource usage in real-world programs, compared with two state-of-the-art fuzzing tools (AFL and MemLock).

Automatic configuration tuning helps users who intend to improve software performance. However, the auto-tuners are limited by the huge configuration search space. More importantly, they focus only on performance improvement while being unaware of other important user intentions (e.g., reliability, security). To reduce the search space, researchers mainly focus on pre-selecting performance-related parameters which requires a heavy stage of dynamically running under different configurations to build performance models. Given that other important user intentions are not paid attention to, we focus on guiding users in pre-selecting performance-related parameters in general while warning about side-effects on non-performance intentions. We find that the configuration document often, if it does not always, contains rich information about the parameters' relationship with diverse user intentions, but documents might also be long and domain-specific.

Safety and robustness properties are highly required for neural networks deployed in safety-critical applications. Current complete verification techniques of these properties suffer from the lack of efficiency and effectiveness. In this article, we present an efficient complete approach to verify safety and robustness properties of neural networks through incrementally determinizing activation states of neurons. The key idea is to generate constraints via layerwised splitting that make activation states of hidden neurons become deterministic efficiently. These constraints are then utilized for refining inputs systematically so that abstract analysis over the refined input can be more precise. Our approach decomposes a verification problem into a set of subproblems via layerwised input space splitting. The property is then checked on each subproblem, where the activation states of at least one hidden neurons will be determinized. Further checking is accelerated by constraint-guided input refinement. We have implemented a parallel tool called LayerSAR to verify safety and robustness properties of ReLU neural networks in a sound and complete way, and evaluated it extensively on several benchmark sets. Experimental results show that our approach is promising, compared with complete tools, such as Planet, Neurify, Marabou, ERAN, Venus, Venus2, and nnenum in verifying safety and robustness properties on the benchmarks.

Multi-agent coordination tends to benefit from efficient communication, where cooperation often happens based on exchanging information about what the agents intend to do, i.e. intention sharing. It becomes a key problem to model the intention by some proper abstraction. Currently, it is either too coarse such as final goals or too fined as primitive steps, which is inefficient due to the lack of modularity and semantics. In this paper, we design a novel multi-agent coordination protocol based on subgoal intentions, defined as the probability distribution over feasible subgoal sequences. The subgoal intentions encode macro-action behaviors with modularity so as to facilitate joint decision making at higher abstraction. Built over the proposed protocol, we present Dec-SGTS (Decentralized Sub-Goal Tree Search) to solve decentralized online multi-agent planning hierarchically and efficiently. Each agent runs Dec-SGTS asynchronously by iteratively performing three phases including local sub-goal tree search, local subgoal intention update and global subgoal intention sharing. We conduct the experiments on courier dispatching problem, and the results show that Dec-SGTS achieves much better reward while enjoying a significant reduction of planning time and communication cost compared with Dec-MCTS (Decentralized Monte Carlo Tree Search).

Linear programming is a key technique for analysis and verification of numerical properties in programs, neural networks, etc. In particular, in program analysis based on abstract interpretation, many numerical abstract domains (such as Template Constraint Matrix, constraint-only polyhedra, etc.) are designed on top of linear programming. However, most state-of-the-art linear programming solvers use floating-point arithmetic in their implementations, leading to an approximate result that may be unsound. On the other hand, the solvers implemented using exact arithmetic are too costly. To this end, this paper focuses on advancing rigorous linear programming techniques based on floating-point arithmetic for building sound and efficient program analysis. Particularly, as a supplement to existing techniques, we present a novel rigorous linear programming technique based on Fourier-Mozkin elimination. On this basis, we implement a tool, namely, RlpSolver, combining our technique with existing techniques to lift effectiveness of rigorous linear programming in the scene of analysis and verification. Experimental results show that our technique is complementary to existing techniques, and their combination (RlpSolver) can achieve a better trade-off between cost and precision via heuristic rules.

Applications depend on libraries to avoid reinventing the wheel. Libraries may have incompatible changes during evolving. As a result, applications will suffer from compatibility failures. There has been much research on addressing detecting incompatible changes in libraries, or helping applications co-evolve with the libraries. The existing solution helps the latest application version work well against the latest library version as an afterthought. However, end users have already been suffering from the failures and have to wait for new versions. In this paper, we propose DepOwl, a practical tool helping users prevent compatibility failures. The key idea is to avoid using incompatible versions from the very beginning. We evaluated DepOwl on 38 known compatibility failures from StackOverflow, and DepOwl can prevent 35 of them. We also evaluated DepOwl using the software repository shipped with Ubuntu-19.10. DepOwl detected 77 unknown dependency bugs, which may lead to compatibility failures.

Despite the surges of deep learning-based method in dynamic scene deblurring achieves good performance, the challenges still remain a lot: (a) the running speed is far from the requirement of processing; (b) there will be inevitable information loss along with the deepening of network layers, which will further lead to the deterioration of the quality of the restored pictures. To deal with these challenges, we propose a novel learning-based model. In our method, we integrate two mechanisms for the generator based on the Generative Adversarial Nets (GAN). First, we develop the Enhanced Feature Fusion (EFF) mechanism which aims at providing multi-layer feature information to assist the image restoration. We further design Feature Multi-distillation (FMD) mechanism to filter and well fuse the multi-scale feature maps. By integrating the two mechanisms, the high-level feature maps can be progressively refined and the detailed semantic information can be properly utilized. In addition, we use the double-scale discriminator architecture which could enables the network to observe the image from the perspective of local and global respectively and obtain overall information for the whole image restoration. Extensive experimental results on the GOPRO and Kohler datasets show that our method can approach comparably to the state-of-the-arts in terms of accuracy while consuming much less inference time, which demonstrates that our method acquiring a better trade off between image restoration quality and running speed.

It is widely desired to precisely predict bounds of resource usages statically in a program, particularly when the program runs in resource-limited contexts. The resource bound problem becomes more challenging for C programs due to the allowed flexible manipulations on dynamically allocated resources in C. In this paper, we present a static analysis approach to deriving the bounds of dynamically allocated resources for C programs. The key idea is to combine numerical value analysis with pointer analysis under the unified framework of abstract interpretation. First, to track resource usage, we intro-duce auxiliary numerical variables to model the resource usage due to resource-manipulating functions such as allocation and deallocation. Second, to handle resource-manipulating functions involving pointers as parameters or return values, we propose a pointer analysis approach designed specifically for resource bound analysis, and combine it with numerical value analysis, to handle pointer arithmetics, dynamic allocation and deallocation, etc. Then, we infer the value bound of auxiliary resource-usage modeling variables to predict resource bounds at each program location. We have implemented our approach in a tool called DARB and conducted experiments on a set of benchmarks extracted from real-world programs. The results show that DARB can deal with C programs with complex resource manipulations.

Symbolic execution is powered by constraint solving. The advancement of constraint solving boosts the development and the applications of symbolic execution. Modern SMT solvers provide the mechanism of solving strategy that allows the users to control the solving procedure, which significantly improves the solver's generalization ability. We observe that the symbolic executions of different programs are actually different constraint solving problems. Therefore, we propose synthesizing a solving strategy for a program to fit the program's symbolic execution best. To achieve this, we divide symbolic execution into two stages. The SMT formulas solved in the first stage are used to online synthesize a solving strategy, which is then employed during the constraint solving in the second stage. We propose novel synthesis algorithms that combine offline trained deep learning models and online tuning to synthesize the solving strategy. The algorithms balance the synthesis overhead and the improvement achieved by the synthesized solving strategy.

Configuration error injection testing (CEIT) could systematically evaluate software reliability and diagnosability to runtime configuration errors. This paper explores the challenges and opportunities of applying CEIT technique. We build an extensible, highly-modularized CEIT framework named CeitInspector to experiment with various CEIT techniques. Using CeitInspector, we quantitatively measure the effectiveness and efficiency of CEIT using six mature and widely-used server applications. During this process, we find a fair number of test cases are left unstudied by the prior research work. The injected configuration errors in these cases often indicate latent misconfigurations, which might be ticking time bombs in the system and lead to severe damage. We conduct an in-depth study regarding these cases to reveal the root causes, and explore possible remedies. Finally, we come up with actionable suggestions guided by our study to improve the effectiveness and efficiency of the existing CEIT techniques.

Parsing code exists extensively in software. Symbolic execution of complex parsing programs is challenging. The inputs generated by the symbolic execution using the byte-level symbolization are usually rejected by the parsing program, which dooms the effectiveness and efficiency of symbolic execution. Complex parsing programs usually adopt token-based input grammar checking. A token sequence represents one case of the input grammar. Based on this observation, we propose grammar-agnostic symbolic execution that can automatically generate token sequences to test complex parsing programs effectively and efficiently. Our method's key idea is to symbolize tokens instead of input bytes to improve the efficiency of symbolic execution. Technically, we propose a novel two-stage algorithm: the first stage collects the byte-level constraints of token values; the second stage employs token symbolization and the constraints collected in the first stage to generate the program inputs that are more possible to pass the parsing code.

Array constraints are prevalent in analyzing a program with symbolic execution. Solving array constraints is challenging due to the complexity of the precise encoding for arrays. In this work, we propose to synergize symbolic execution and array constraint solving. Our method addresses the difficulties in solving array constraints with novel ideas. First, we propose a lightweight method for pre-checking the unsatisfiability of array constraints based on integer linear programming. Second, observing that encoding arrays at the byte-level introduces many redundant axioms that reduce the effectiveness of constraint solving, we propose type and interval aware axiom generation. Note that the type information of array variables is inferred by symbolic execution, whereas interval information is calculated through the above pre-checking step. We have implemented our methods based on KLEE and its underlying constraint solver STP and conducted large-scale experiments on 75 real-world programs. The experimental results show that our method effectively improves the efficiency of symbolic execution. Our method solves 182.56% more constraints and explores 277.56% more paths on average under the same time threshold.

The classic linear (technically, affine) equality abstract domain, which can infer linear equality relations among variables of a program automatically, is one of the earliest and fundamental abstract domains. As a lightweight relational abstract domain, it has been widely used in program analysis. However, it cannot express non-convex properties that appear naturally due to the inherent disjunctive behaviors in a program. In this paper, we introduce a new abstract domain, namely the abstract domain of linear absolute value equalities, which generalizes the linear equality abstract domain with absolute value terms of variables. More clearly, we leverage the absolute value function to design the new abstract domain for discovering linear equality relations among values and absolute values of program variables. The new abstract domain can be used to infer piecewise linear behaviors (e.g., due to conditional branches, absolute value function calls, max/min function calls, etc.) in a program. Experimental results of our prototype are encouraging: In practice, the new abstract domain can find interesting piece-wise linear invariants that are non-convex and out of the expressiveness of the linear equality domain.

Recent years have witnessed the significant rise of Deep Learning (DL) techniques applied to source code. Researchers exploit DL for a multitude of tasks and achieve impressive results. However, most tasks are explored separately, resulting in a lack of generalization of the solutions. In this work, we propose MulCode, a multi-task learning approach for source code understanding that learns unified representation space for tasks, with the pre-trained BERT model for the token sequence and the Tree-LSTM model for abstract syntax trees. Furthermore, we integrate two source code views into a hybrid representation via the attention mechanism and set learnable uncertainty parameters to adjust the tasks' relationship.We train and evaluate MulCode in three downstream tasks: comment classification, author attribution, and duplicate function detection. In all tasks, MulCode outperforms the state-of-the-art techniques. Moreover, experiments on three unseen tasks demonstrate the generalization ability of MulCode compared with state-of-the-art embedding methods.

No abstract available.

The runtime environment and workload of software are constantly changing, requiring users to make appropriate adjustments to accommodate these changes. The runtime configuration, however, as the interface for users to manipulate software behavior often requires domain-specific knowledge to understand. This usually results in users spending a considerable amount of time wading through document and user manuals trying to understand the runtime configuration. In this paper, we study the possibility of understanding the intention of runtime configuration options through their documents, even sometimes it is difficult for users to understand. Based on these studies, we classify the runtime configuration option’s intention into six categories. Accordingly, we design runtime Configuration Intention Classifier (CIC), a supervised approach based on CNN to classify the runtime configuration option’s intention according to its document. CIC integrates the features of runtime configuration names and descriptions according to different levels of granularity and predicts the intention of runtime configuration options accordingly. Extensive experiments show that our approach can achieve an accuracy of 85.6% and outperform nine comparative approaches by up to 16.6% over the dataset we customized.

Unsupervised domain adaptation (UDA) has emerged as an effective paradigm for reducing the huge manual annotation cost for Person Re-Identification (Re-ID). Many of the recent UDA methods for Re-ID are clustering-based and select all the pseudo-label samples in each iteration for the model training. However, there are many wrong labeled samples that will mislead the model optimization under this circumstance. To solve this problem, we propose a Progressive Unsupervised Domain Adaptation (PUDA) framework for image-based Person Re-ID to reduce the negative effect of wrong pseudo-label samples on the model training process. Specifically, we first pretrain a CNN model on a labeled source dataset, then finetune the model on unlabeled target dataset with the following three steps iteratively: 1) estimating pseudo-labels for all the images in the target dataset with the model trained in the last iteration; 2) extending the training set by adding pseudo-label samples with higher label confidence; 3) updating the CNN model with the expanded training set in a supervised manner. During the iteration process, the number of pseudo-label samples added increased progressively. In particular, a Moderate Initial Selections (MIS) strategy for pseudo-label sampling is also proposed to reduce the negative impacts of random noise features in the early iterations and mislabeled samples in the late iterations on the model. The proposed framework with MIS strategy is validated on the Duke-to-Market, Market-to-Duke unsupervised domain adaptation tasks and achieves improvements of 4.2 points (absolute, i.e., 80.0% vs. 75.8%) and 1.7 points (absolute, i.e., 70.7% vs. 69.0%) in mAP correspondingly.

Message passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). In this work, we present MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for automatically verifying MPI programs with non-blocking operations. MPI-SV combines symbolic execution and model checking in a synergistic way to tackle the challenges in MPI program verification. The synergy improves the scalability and enlarges the scope of verifiable properties. We have implemented MPI-SV1 and evaluated it with 111 real-world MPI verification tasks. The pure symbolic execution-based technique successfully verifies 61 out of the 111 tasks (55%) within one hour, while in comparison, MPI-SV verifies 100 tasks (90%). On average, compared with pure symbolic execution, MPI-SV achieves 19x speedups on verifying the satisfaction of the critical property and 5x speedups on finding violations.

Fine-grained entity typing (FET) is a fundamental task for various entity-leveraging applications. Although great success has been made, existing systems still have challenges in handling noisy samples in training data introduced by distant supervision methods. To address these noise, previous studies either focus on processing the clean samples (i,e., have only one label) and noisy samples (i,e., have multiple labels) with different strategies or filtering the noisy labels based on the assumption that the distantly-supervised label set certainly contains the correct type label. In this paper, we propose a probabilistic automatic relabeling method which treats all training samples uniformly. Our method aims to estimate the pseudo-truth label distribution of each sample, and the pseudo-truth distribution will be treated as part of trainable parameters which are jointly updated during the training process. The proposed approach does not rely on any prerequisite or extra supervision, making it effective on real applications. Experiments on several benchmarks show that our method outperforms previous approaches and alleviates the noisy labeling problem.

Performance bugs are often hard to detect due to their non fail-stop symptoms. Existing debugging techniques can only detect performance bugs with known patterns (e.g., inefficient loops). The key reason behind this incapability is the lack of a general test oracle. Here, we argue that the performance (e.g., throughput, latency, execution time) expectation of configuration can serve as a strong oracle candidate for performance bug detection. First, prior work shows that most performance bugs are related to configurations. Second, the configuration change reflects common expectation on performance changes. If the actual performance is contrary to the expectation, the related code snippet is likely to be problematic.

The robustness of deep neural network (DNN) is critical and challenging to ensure. In this paper, we propose a general data-oriented mutation framework, called Styx, to improve the robustness of DNN. Styx generates new training data by slightly mutating the training data. In this way, Styx ensures the DNN's accuracy on the test dataset while improving the adaptability to small perturbations, i.e., improving the robustness. We have instantiated Styx for image classification and proposed pixel-level mutation rules that are applicable to any image classification DNNs. We have applied Styx on several commonly used benchmarks and compared Styx with the representative adversarial training methods. The preliminary experimental results indicate the effectiveness of Styx.

Path explosion and constraint solving are two challenges to symbolic execution's scalability. Symbolic execution explores the program's path space with a searching strategy and invokes the underlying constraint solver in a black-box manner to check the feasibility of a path. Inside the constraint solver, another searching procedure is employed to prove or disprove the feasibility. Hence, there exists the problem of double searchings in symbolic execution. In this paper, we propose to unify the double searching procedures to improve the scalability of symbolic execution. We propose Multiplex Symbolic Execution (MuSE) that utilizes the intermediate assignments during the constraint solving procedure to generate new program inputs. MuSE maps the constraint solving procedure to the path exploration in symbolic execution and explores multiple paths in one time of solving. We have implemented MuSE on two symbolic execution tools (based on KLEE and JPF) and three commonly used constraint solving algorithms. The results of the extensive experiments on real-world benchmarks indicate that MuSE has orders of magnitude speedup to achieve the same coverage.

Symbolic execution is still facing the scalability problem caused by path explosion and constraint solving overhead. The recently proposed MuSE framework supports exploring multiple paths by generating partial solutions in one time of solving. In this work, we improve MuSE from two aspects. Firstly, we use a light-weight check to reduce redundant partial solutions for avoiding the redundant executions having the same results. Secondly, we introduce online learning to devise an adaptive search strategy for the target programs. The preliminary experimental results indicate the promising of the proposed methods.

Domain adaptation aims at learning a predictive model that can generalize to a new target domain different from the source (training) domain. To mitigate the domain gap, adversarial training has been developed to learn domain invariant representations. State-of-the-art methods further make use of pseudo labels generated by the source domain classifier to match conditional feature distributions between the source and target domains. However, if the target domain is more complex than the source domain, the pseudo labels are unreliable to characterize the class-conditional structure of the target domain data, undermining prediction performance. To resolve this issue, we propose a Pairwise Similarity Regularization (PSR) approach that exploits cluster structures of the target domain data and minimizes the divergence between the pairwise similarity of clustering partition and that of pseudo predictions. Therefore, PSR guarantees that two target instances in the same cluster have the same class prediction and thus eliminate the negative effect of unreliable pseudo labels. Extensive experimental results show that our PSR method significantly boosts the current adversarial domain adaptation methods by a large margin on four visual benchmarks. In particular, PSR achieves a remarkable improvement of more than 5% over the state-of-the-art on several hard-to-transfer tasks.

Symbolic execution is an effective way of systematically exploring the search space of a program, and is often used for automatic software testing and bug finding. The program to be analyzed is usually compiled into a binary or an intermediate representation, on which symbolic execution is carried out. During this process, compiler optimizations influence the effectiveness and efficiency of symbolic execution. However, to the best of our knowledge, there exists no work on compiler optimization recommendation for symbolic execution with respect to (w.r.t.) modified condition/decision coverage (MC/DC), which is an important testing coverage criterion widely used for mission-critical software. This study describes our use of a state-of-the-art symbolic execution tool to carry out extensive experiments to study the impact of compiler optimizations on symbolic execution w.r.t. MC/DC. The results indicate that instruction combining (IC) optimization is the important and dominant optimization for symbolic execution w.r.t. MC/DC. We designed and implemented a support vector machine based optimization recommendation method w.r.t. IC (denoted as auto). The experiments on two standard benchmarks (Coreutils and NECLA) showed that auto achieves the best MC/DC on 67.47% of Coreutils programs and 78.26% of NECLA programs.

In this perspective article, we first recall the historic background of human-cyber-physical systems (HCPSs), and then introduce and clarify important concepts. We discuss the key challenges in establishing the scientific foundation from a system engineering point of view, including (1) complex heterogeneity, (2) lack of appropriate abstractions, (3) dynamic black-box integration of heterogeneous systems, (4) complex requirements for functionalities, performance, and quality of services, and (5) design, implementation, and maintenance of HCPS to meet requirements. Then we propose four research directions to tackle the challenges, including (1) abstractions and computational theory of HCPS, (2) theories and methods of HCPS architecture modelling, (3) specification and verification of model properties, and (4) software-defined HCPS. The article also serves as the editorial of this special section on cyber-physical systems and summarises the four articles included in this special section.

Numerical computation is often involved in software of embedded control systems, cyber-physical systems, artificial neural network systems, big data processing systems, etc. Automatically discovering numerical loop invariants is fundamental for checking the safety of such software. Abstract interpretation provides a framework to automatically discover sound invariants but which may be not precise enough due to over-approximations. One major source of precision loss is due to the limited linear expressiveness of most widely used numerical abstract domains and the widening operation. This becomes more serious when analyzing all variables simultaneously as a whole for programs that involve nonlinear behaviors. Based on the observation that the dependency among variables in a loop can be hierarchical, in this article, we propose a hierarchical static analysis to analyze a loop by utilizing relaxed abstract transformers. The main idea is to first partition all variables involved in a loop into different hierarchical layers, then compute invariants over the variables layer by layer in a bottom-up manner. During the iterative process, the computed invariants over lower layer variables are then used to relax transfer functions when analyzing the higher layer variables. One benefit of our method lies in that it can generate linear invariants to soundly enclose nonlinear behaviors in a loop. Finally, we present encouraging experimental results on benchmark programs involving nonlinear behaviors.

Bounded model checking is among the most efficient techniques for the automated verification of concurrent programs. However, due to the nondeterministic thread interleavings, a large and complex formula is usually required to give an exact encoding of all possible behaviors, which significantly limits the scalability. Observing that the large formula is usually dominated by the exact encoding of the scheduling constraint, this paper proposes a novel scheduling constraint based abstraction refinement method for multi-threaded C program verification. Our method is both efficient in practice and complete in theory, which is challenging for existing techniques. To achieve this, we first proposed an effective and powerful technique which works well for nearly all benchmarks we evaluated. We have proposed the notion of Event Order Graph (EOG), and have devised two graph-based algorithms over EOG for counterexample validation and refinement generation, which can often obtain a small yet effective refinement constraint. Then, to ensure completeness, our method was enhanced with two constraint-based algorithms for counterexample validation and refinement generation. Experimental results on SV-COMP 2017 benchmarks and two real-world server systems indicate that our method is promising and significantly outperforms the state-of-the-art tools.

In this work, we focus on complex question semantic parsing and propose a novel Hierarchical Semantic Parsing (HSP) method, which utilizes the decompositionality of complex questions for semantic parsing.Our model is designed within a three-stage parsing architecture based on the idea of decompositionintegration.In the first stage, we propose a question decomposer which decomposes a complex question into a sequence of subquestions.In the second stage, we design an information extractor to derive the type and predicate information of these questions.In the last stage, we integrate the generated information from previous stages and generate a logical form for the complex question.We conduct experiments on COMPLEXWE-BQUESTIONS which is a large scale complex question semantic parsing dataset, results show that our model achieves significant improvement compared to state-of-the-art methods.

In this paper, we propose a novel pretrainingbased encoder-decoder framework, which can generate the output sequence based on the input sequence in a two-stage manner.For the encoder of our model, we encode the input sequence into context representations using BERT.For the decoder, there are two stages in our model, in the first stage, we use a Transformer-based decoder to generate a draft output sequence.In the second stage, we mask each word of the draft sequence and feed it to BERT, then by combining the input sequence and the draft representation generated by BERT, we use a Transformer-based decoder to predict the refined word for each masked position.To the best of our knowledge, our approach is the first method which applies the BERT into text generation tasks.As the first step in this direction, we evaluate our proposed method on the text summarization task.Experimental results show that our model achieves new state-of-the-art on both CNN/Daily Mail and New York Times datasets.

Program verification is one of the most important methods to ensuring the correctness of concurrent programs. However, due to the path explosion problem, concurrent program verification is usually time consuming, which hinders its scalability to industrial programs. Parallel processing is a mainstream technique to deal with those problems which require mass computing. Hence, designing parallel algorithms to improve the performance of concurrent program verification is highly desired. This paper focuses on parallelization of the abstraction refinement technique, one of the most efficient techniques for concurrent program verification. We present a parallel refinement framework which employs multiple engines to refine the abstraction in parallel. Different from existing work which parallelizes the search process, our method achieves the effect of parallelization by refinement constraint and learnt clause sharing, so that the number of required iterations can be significantly reduced. We have implemented this framework on the scheduling constraint based abstraction refinement method, one of the best methods for concurrent program verification. Experiments on SV-COMP 2018 show the encouraging results of our method. For those complex programs requiring a large number of iterations, our method can obtain a linear reduction of the iteration number and significantly improve the verification performance.

The performance of decentralized multi-agent systems tends to benefit from information sharing and its effective utilization. However, too much or unnecessary sharing may hinder the performance due to the delay, instability and additional overhead of communications. Aiming to a satisfiable coordination performance, one would prefer the cost of communications as less as possible. In this paper, we propose an approach for improving the sharing utilization by integrating information sharing with prediction in decentralized planning. We present a novel planning algorithm by combining decision sharing and prediction based on decentralized Monte Carlo Tree Search called Dec-MCTS-SP. Each agent grows a search tree guided by the rewards calculated by the joint actions, which can not only be sampled from the shared probability distributions over action sequences, but also be predicted by a sufficiently-accurate and computationally-cheap heuristics-based method. Besides, several policies including sparse and discounted UCT and DIY-bonus are leveraged for performance improvement. We have implemented Dec-MCTS-SP in the case study on multi-agent information gathering under threat and uncertainty, which is formulated as Decentralized Partially Observable Markov Decision Process (Dec-POMDP). The factored belief vectors are integrated into Dec-MCTS-SP to handle the uncertainty. Comparing with the random, auction-based algorithm and Dec-MCTS, the evaluation shows that Dec-MCTS-SP can reduce communication cost significantly while still achieving a surprisingly higher coordination performance.

Most software systems frequently encounter errors when interacting with their environments. When errors occur, error-handling code must execute flawlessly to facilitate system recovery. Implementing correct error handling is repetitive but non-trivial, and developers often inadvertently introduce bugs into error-handling code. Existing tools require correct error specifications to detect error-handling bugs. Manually generating error specifications is error-prone and tedious, while automatically mining error specifications is hard to achieve a satisfying accuracy. In this paper, we propose EH-Miner, a novel and practical tool that can automatically detect error-handling bugs without the need for error specifications. Given a function, EH-Miner mines its error-handling rules when the function is frequently checked by an equivalent condition, and handled by the same action. We applied EH-Miner to 117 applications across 15 software domains. EH-Miner mined error-handling rules with the precision of 91.1% and the recall of 46.9%. We reported 142 bugs to developers, and 106 bugs had been confirmed and fixed at the time of writing. We further applied EH-Miner to Linux kernel, and reported 68 bugs for kernel-4.17, of which 42 had been confirmed or fixed.

Software encounters ungraceful exits due to either bugs in the interrupt/signal handler code or the intention of developers to debug the software. Users may suffer from ”weird” problems caused by leftovers of the ungraceful exits. A common practice to fix these problems is rebooting, which wipes away the stale state of the software. This solution, however, is heavyweight and often leads to poor user experience because it requires restarting other normal processes. In this paper, we design SafeExit, a tool that can automatically detect and pinpoint the root causes of the problems caused by ungraceful exits, which can help users fix the problems using lightweight solutions. Specifically, SafeExit checks the program exit behaviors in the case of an interrupted execution against its expected exit behaviors to detect the missing cleanup behaviors required for avoiding the ungraceful exit. The expected behaviors are obtained by monitoring the program exit under a normal execution. We apply SafeExit to 38 programs across 10 domains. SafeExit finds 133 types of cleanup behaviors from 36 programs and detects 2861 missing behaviors from 292 interrupted executions. To predict missing behaviors for unseen input scenarios, SafeExit trains prediction models using a set of sampled input scenarios. The results show that SafeExit is accurate with an average F-measure of 92.5%.

Verifying the regular properties of programs has been a significant challenge. This paper tackles this challenge by presenting symbolic regular verification (SRV) that offers significant speedups over the state-of-the-art. SRV is based on dynamic symbolic execution (DSE) and enabled by novel techniques for mitigating path explosion: (1) a regular property-oriented path slicing algorithm, and (2) a synergistic combination of property-oriented path slicing and guiding. Slicing prunes redundant paths, while guiding boosts the search for counterexamples. We have implemented SRV for Java and evaluated it on 15 real-world open-source Java programs (totaling 259K lines of code). Our evaluation results demonstrate the effectiveness and efficiency of SRV. Compared with the state-of-the-art --- pure DSE, pure guiding, and pure path slicing --- SRV achieves average speedups of more than 8.4X, 8.6X, and 7X, respectively, making symbolic regular property verification significantly more practical.

Log statements are widely used for postmortem debugging. Despite the importance of log messages, it is difficult for developers to establish good logging practices. There are two main reasons for this. First, there are no rigorous specifications or systematic processes to guide the practices of software logging. Second, logging code co-evolves with bug fixes or feature updates. While previous works on log enhancement have successfully focused on the first problem, they are hard to solve the latter. For taking the first step towards solving the second problem, this paper is inspired by code clones and assumes that logging code with similar context is pervasive in software and deserves similar modifications. To verify our assumptions, we conduct an empirical study on eight open-source projects. Based on the observation, we design and implement LogTracker, an automatic tool that can predict log revisions by mining the correlation between logging context and modifications. With an enhanced modeling of logging context, LogTracker is able to guide more intricate log revisions that cannot be covered by existing tools. We evaluate the effectiveness of LogTracker by applying it to the latest version of subject projects. The results of our experiments show that LogTracker can detect 199 instances of log revisions. So far, we have reported 25 of them, and 6 have been accepted.

Scheduling constraint based abstraction refinement (SCAR) is one of the most efficient methods for verifying programs under sequential consistency (SC). However, most multi-processor architectures implement weak memory models (WMMs) in order to improve the performance of a program. Due to the nondeterministic execution of those memory operations by the same thread, the behavior of a program under WMMs is much more complex than that under SC, which significantly increases the verification complexity. This paper elegantly extends the SCAR method to WMMs such as TSO and PSO. To capture the order requirements of an abstraction counterexample under WMMs, we have enriched the event order graph (EOG) of a counterexample such that it is competent for both SC and WMMs. We have also proposed a unified EOG generation method which can always obtain a minimal EOG efficiently. Experimental results on a large set of multi-threaded C programs show promising results of our method. It significantly outperforms state-of-the-art tools, and the time and memory it required to verify a program under TSO and PSO are roughly comparable to that under SC.

This paper presents the Y ogar - CBMC tool for verification of multi-threaded C programs. It employs a scheduling constraint based abstraction refinement method for bounded model checking of concurrent programs. To obtain effective refinement constraints, we have proposed the notion of Event Order Graph (EOG) , and have devised two graph-based algorithms over EOG for counterexample validation and refinement generation. The experiments in SV-COMP 2017 show the promising results of our tool.

This paper studies Bounded Model Checking (BMC) of invariant properties on compositional systems. To alleviate the path explosion problem resulting from interleaving, an ideal approach is to let the system execute in true-concurrency. However, since it is difficult for the true-concurrency execution manner to obtain all reachable global states, this technique has been rarely employed to verify those properties requiring to check all reachable global states—such as invariant properties. Verification of such properties still adheres to the interleaving semantics. Observed that even for properties such as invariants, it is possible to verify them via checking only a fraction of the global states, this paper presents a true-concurrency encoding for invariant property verification of compositional systems. The crucial innovation is a macro-step technique, which executes a sequence of consecutive transitions in true-concurrency. With this technique, we are able to (1) significantly reduce the exponential number of paths due to interleaving, and (2) greatly cut down the number of SAT calls required for BMC to verify the property. Experimental results of real problems show speed increases from 4.8 to 2957 times that of the standard verification method.

User request trace-oriented monitoring is an effective method to improve the reliability of cloud services. However, there are some difficulties in getting useful traces in practice, which hinder the development of trace-oriented monitoring research. In this paper, we release a fine-grained user request-centric open trace data set, called TraceBench, which is collected in a real-world cloud storage service deployed in a real environment. When collecting, we consider different scenarios, involving multiple scales of clusters, different kinds of user requests, various speeds of workloads, many types of injected faults, etc. To validate the usability and authenticity, we have employed TraceBench in several trace-oriented monitoring topics, such as anomaly detection, performance problem diagnosis, and temporal invariant mining. The results show that TraceBench well supports these research topics. In addition, we have also carried out an extensive data analysis based on TraceBench, which validates the high quality of the data set.

It is challenging to effectively check a regular property of a program. This paper presents RGSE, a regular property guided dynamic symbolic execution (DSE) engine, for finding a program path satisfying a regular property as soon as possible. The key idea is to evaluate the candidate branches based on the history and future information, and explore the branches along which the paths are more likely to satisfy the property in priority. We have applied RGSE to 16 real-world open source Java programs, totaling 270K lines of code. Compared with the state-of-the-art, RGSE achieves two orders of magnitude speedups for finding the first target path. RGSE can benefit many research topics of software testing and analysis, such as path-oriented test case generation, typestate bug finding, and performance tuning. The demo video is at: https://youtu.be/7zAhvRIdaUU, and RGSE can be accessed at: http://jrgse.github.io.

Embedded software often involves intensive numerical computations and suffers from a number of runtime errors. The technique of numerical static analysis is of practical importance for checking the correctness of embedded software. However, most of the existing approaches of numerical static analysis consider sequential programs, while interrupts are a commonly used facility that introduces concurrency in embedded systems. Therefore, a numerical static analysis approach is highly desired for embedded software with interrupts. In this article, we propose a static analysis approach specifically for interrupt-driven programs based on sequentialization techniques. We present a method to sequentialize interrupt-driven programs into nondeterministic sequential programs according to the semantics of interrupts. The key benefit of using sequentialization is the ability to leverage the power of state-of-the-art analysis and verification techniques for sequential programs to analyze interrupt-driven programs, for example, the power of numerical abstract interpretation to analyze numerical properties of the sequentialized programs. Furthermore, to improve the analysis precision and scalability, we design specific abstract domains to analyze sequentialized interrupt-driven programs by considering their specific features. Finally, we present encouraging experimental results obtained by our prototype implementation.

MPI is widely used in high performance computing. In this extended abstract, we report our current status of analyzing MPI programs. Our method can provide coverage of both input and non-determinism for MPI programs with mixed blocking and non-blocking operations. In addition, to improve the scalability further, a deadlock-oriented guiding method for symbolic execution is proposed. We have implemented our methods, and the preliminary experimental results are promising.

A challenging problem in software engineering is to check if a program has an execution path satisfying a regular property. We propose a novel method of dynamic symbolic execution (DSE) to automatically find a path of a program satisfying a regular property. What makes our method distinct is when exploring the path space, DSE is guided by the synergy of static analysis and dynamic analysis to find a target path as soon as possible. We have implemented our guided DSE method for Java programs based on JPF and WALA, and applied it to 13 real-world open source Java programs, a total of 225K lines of code, for extensive experiments. The results show the effectiveness, efficiency, feasibility and scalability of the method. Compared with the pure DSE on the time to find the first target path, the average speedup of the guided DSE is more than 258X when analyzing the programs that have more than 100 paths.

Currently, the performance problems of software systems gets more and more attentions. Among various diagnosis methods based on system traces, principal component analysis (PCA) based methods are widely used due to the high accuracy of the diagnosis results and requiring no specific domain knowledge. However, according to our experiments, we have validated several shortcomings existed in PCA-based methods, including requiring traces with a same call sequence, inefficiency when the traces are long, and missing performance problems. To cope with these issues, we introduce a segmentation based online diagnosis method in this poster.

Trace-oriented monitoring is one of the main methods for monitoring cloud systems. However, there is no free trace data set available, which hinders the development of trace-oriented monitoring. Therefore, we want to collect a trace data set in a real environment and make it free. During collection, many aspects are considered, including cluster sizes, user requests, workload speeds, injected faults, etc., to simulate different situations. The structure of this data set is well-designed. We believe that this data set will be helpful for the research of trace-oriented monitoring.

Asynchrony based overlapping of computation and communication is commonly used in MPI applications. However, this overlapping introduces synchronization errors frequently in asynchronous MPI programming. In this paper, we propose a symbolic execution based method for detecting input-related synchronization errors. The path space of an MPI program is systematically explored, and the related operations of the synchronization errors in the program are checked specifically. In addition, two optimizations are proposed to improve the efficiency. We have implemented our method as a prototype tool based on the symbolic executor Cloud9. The results of the extensive experiments indicate the effectiveness of our method.

User request trace-oriented monitoring is an effective method to improve the reliability of cloud systems. However, there are some difficulties in getting traces in practice, which hinder the development of trace-oriented monitoring research. In this paper, we release a fine-grained user request-centric open trace data set, called Trace Bench, collected on a real world cloud storage system deployed in a real environment. During collecting, many aspects are considered to simulate different scenarios, including cluster size, request type, workload speed, etc. Besides recording the traces when the monitored system is running normally, we also collect the traces under the situation with faults injected. With a mature injection tool, 14 faults are introduced, including function faults and performance faults. The traces in Trace Bench are clustered in different files, where each file corresponds to a certain scenario. The whole collection work lasted for more than half a year, resulting in more than 360, 000 traces in 361 files. In addition, we also employ several applications based on Trace Bench, which validate the helpfulness of Trace Bench for the field of trace-oriented monitoring.

Nowadays, more and more scientific applications are moving to cloud computing. The optimal deployment of scientific applications is critical for providing good services to users. Scientific applications are usually topology-aware applications. Therefore, considering the topology of a scientific application during the development will benefit the performance of the application. However, it is challenging to automatically discover and make use of the communication pattern of a scientific application while deploying the application on cloud. To attack this challenge, in this paper, we propose a framework to discover the communication topology of a scientific application by pre-execution and multi-scale graph clustering, based on which the deployment can be optimized. Comprehensive experiments are conducted by employing a well-known MPI benchmark and comparing the performance of our method with those of other methods. The experimental results show the effectiveness of our topology-aware deployment method.

Heap-manipulating programs allow flexible manipulations over dynamically allocated, shared, and mutable heap cells via pointers that point to not only linked data structures but also their pointer fields. Therefore, memory leak detection for these programs requires precise field-sensitive pointer alias information, which make the problem more challenging. In this paper, we present a field and context sensitive algorithm for detecting memory leaks in heap-manipulating programs. First, we propose a modular heap abstraction based on member-access distances and alias bit-vector domain as the escape model of each procedure, Then, based on procedural summaries characterized by this modular heap abstraction, an efficient context-sensitive memory leak detection is proposed in an on-demand way. Experimental evaluation about a set of large C benchmark programs shows that the proposed approach is scalable with satisfied precision as expected.

Infrastructure-as-a-Service (IaaS) clouds provide on-demand virtual machines (VMs) to users. How to improve the quality of IaaS cloud services is important for service providers. Currently, the VMs in an IaaS cloud are usually deployed with respect to the maximum utilization of resources. In this paper, we propose an online VM optimization method for IaaS clouds. Our method mainly optimizes the VM deployment in IaaS clouds according to the traffics among VMs. VMs are allocated with respect to cabinet capacities at the beginning. At runtime, we monitor the traffics among VMs to get the traffic topology, based on which related VMs are migrated to neighbors to improve performance and reduce the traffics across cabinets. Preliminary simulation experiments are conducted on a well-know simulator, and the experimental results indicate that our method is effective and promising.

Symbolic execution is an effective path oriented and constraint based program analysis technique. Recently, there is a significant development in the research and application of symbolic execution. However, symbolic execution still suffers from the scalability problem in practice, especially when applied to large-scale or very complex programs. In this paper, we propose a new fashion of symbolic execution, named Speculative Symbolic Execution (SSE), to speed up symbolic execution by reducing the invocation times of constraint solver. In SSE, when encountering a branch statement, the search procedure may speculatively explore the branch without regard to the feasibility. Constraint solver is invoked only when the speculated branches are accumulated to a specified number. In addition, we present a key optimization technique that enhances SSE greatly. We have implemented SSE and the optimization technique on Symbolic Pathfinder (SPF). Experimental results on six programs show that, our method can reduce the invocation times of constraint solver by 20.7% to 48.7% (with an average of 29.9%), and save the search time from 23.6% to 43.6% (with an average of 30%).

Strongly promoted by the leading industrial companies, cloud computing becomes increasingly popular in re-cent years. The growth rate of cloud computing surpasses even the most optimistic predictions. A cloud application is a large-scale distributed system that consist a lot of distributed cloud nodes. How to make optimal deployment of cloud applications is a challenging research problem. When deploying a cloud application to the cloud environment, cloud node ranking is one of the most important approaches for selecting optimal cloud nodes for the cloud application. Traditional ranking methods usually rank the cloud nodes based on their QoS values, without considering the communication performance between cloud nodes. However, such kind of node relationship is very important for the communication-intensive cloud applications (e.g., Message Passing Interface (MPI) programs), which have a lot of communications between the selected cloud nodes. In this paper, we propose a novel clustering-based method for selecting optimal cloud nodes for deploying communication-intensive applications to the cloud environment. Our method not only takes into account the cloud node qualities, but also the communication performance between different nodes. We deploy several well-known MPI programs on a real-world cloud and compare our method with other methods. The experimental results show the effectiveness of our cluster-based method.

2011-2012 > Academic research: refereed > Refereed conference paper

The key issue of person name disambiguation is to discover different namesakes in massive web documents rather than simply cluster documents by using textual features. In this paper, we describe a novel person name disambiguation method based on social networks to effectively identify namesakes. The social network snippets in each document are extracted. Then, the namesakes are identified via splicing the social networks of each namesake by using the snippets as a bipartite graph. Experimental results show that our method achieves better result than the top performance of WePS-2 in identifying different namesakes.

Editorial for the special issue of Software: Practice and Experience which consists of six papers that are extended from the best papers of the 10th International Conference on Quality Software (QSIC 2010), Zhangjiajie, China, 14-15 July 2010.

In this paper, we introduce a generic model to deal with the event matching problem of content-based publish/subscribe systems over structured P2P overlays. In this model, we claim that there are three methods (event-oriented, subscription-oriented and hybrid) to make all the matched pairs (event, subscription) meet in a system. By theoretically analyzing the inherent problem of both event-oriented and subscription-oriented methods, we propose PEM (Popularity-based Event Matching), a variant of hybrid method. PEM can achieve better trade-off between event processing load and subscription storage load of a system. PEM has been verified through both mathematical and simulation-based evaluation.

Model abstraction plays an important role in model checking of source codes of programs. Slicing execution is a lightweight symbolic execution procedure to extract the models of C programs in an over-approximated way. In this paper, we present an approach to improving slicing execution with a novel concept called partial weakest precondition (PWP) to alleviate the space explosion problem. PWPs specify the corresponding weakest precondition conservatively by only considering part of program variables. We present how to integrate PWP with slicing execution, which leads to a compact model with much smaller state space compared with the one obtained by the original slicing execution. A new PWP implementation is also presented to avoid possible exponential PWP formula size and support pointers and aliases as well. The distinguished features of the implementation are that it does not need to translate the program to the passive form beforehand, and it supports loops very well. Comparing with slicing execution without PWP, the experimentation on SSL protocol based on the C source code openssl-0.9.6c shows that the state space may be reduced to only 1/10 after applying PWP.

The Internet-based Virtual Computing Environment (iVCE) provides on-demand aggregation and autonomic collaboration mechanisms to facilitate the utilization of autonomous and dynamic Internet resources. Load balancing and fault tolerance are important issues when scheduling those transient resources. In this paper, we propose a mobility mechanism for the migration of various roles of agents in the iVCE platform. The mobility mechanism involves two parts of the iVCE platform: role container layer and event service layer. At the role container layer, a novel approach is proposed to handle the code and data mobility issue. At the event service layer, an efficient routing reconfiguration protocol is proposed based on a publish/subscribe system over DHTs to facilitate task migrations. Certain conditions must be satisfied before the migration of an agent to ensure the correctness of the whole process. Experiments are conducted to evaluate the performance of the mobility mechanism, and the experimental results show that it is suitable for implementing load balancing and fault tolerance in the iVCE.

A program mode is a regular trajectory of the execution of a program that is determined by the values of its input variables. By exploiting program modes, we may make worst-case execution time (WCET) analysis more precise. This paper presents a novel method to automatically find program modes and calculate the WCET estimates of programs. First, the modes of a program will be identified automatically by mode-relevant program slicing, and the precondition will be calculated for each mode using a path-wise test data generation method. Then, for each feasible mode, we show how to calculate its WCET estimate for modern reduced instruction set computer (RISC) processors with caches and pipelines and for traditional complex instruction set computer (CISC) processors. We also present a method to obtain the symbolic expression for each mode for CISC processors. The experimental results show the effectiveness of the method.

The paper presents the ongoing work of studying FMEA method for embedded safely critical software via formal analysis of various dependence relations among software elements, which can fairly improve the automation and precision of both system level and detailed level FMEA. These dependence relations are depicted by the formal models abstracted from software design and implementation, and the FMEA processes for both structural and object-oriented software are proposed respectively. The initial result of case study shows the effectiveness of the approach.

PSL is a kind of temporal logic which uses SEREs as additional formula constructs. We present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. In this paper, we extend the LTL symbolic model checking algorithm to that of APSL, and present a tableau based APSL verification approach. Moreover, we show how to implement this algorithm via the BDD based symbolic approach.

UML dynamic models are important for software analysis and design. Verifying UML dynamic models to find design errors earlier is a key issue for ensuring software quality. Because of the characteristics such as concurrency and hierarchy, model checking of UML Statecharts and collaboration diagrams faces the problem of state explosion. In this paper, UML Statecharts is firstly structurally expressed by hierarchical automata and its semantics for open systems is introduced. Then, the synchronization composition of objects in UML collaboration diagrams is expatiated, based on which the global system behaviors can be constructed. Based on hierarchical automata and simulation relation between semantics structures, the compositional rules for verifying concurrent object systems are proposed. It makes possible that the construction of global state space will be unnecessary in model checking of UML collaboration diagrams. The hierarchical structures of UML Statecharts are also brought into the compositional verification, which makes the model checking of implementation models can be carried out through replacing detailed components by abstract specifications.

The verification of Web services becomes a challenge in software verification. This paper presents a framework for verification of Web service interfaces at various abstraction levels. Its foundation is the interface theory for Web services, in which transaction features are incorporated. Within the framework, one may check non mutual invocation, compatibility and refinement of Web services at signature, conversation and protocol levels. At protocol level, we present a model checking approach to verifying the protocol properties in action set computation tree logic (ASCTL). The paper also discusses the integration of our framework into the Web service development

The paper presents a novel framework for scalable model checking of concurrent C programs. With the idea of verification reuse, it shows an integrated approach to efficient reduction of state space by abstraction, symbolic representation and dynamic partial-order reduction (DPOR) techniques. The framework is founded on an over-approximated model of the concurrent program by variable abstraction, and combines DPOR with lightweight symbolic execution to generate the symbolic conditions for all locations, called -conditions, which are intended for verification reuse. The -conditions of a location are weak approximation of the conditions that must be satisfied at that location so as to guarantee the temporal safety properties to be verified. These conditions will be checked for reusing the previous exploration in verification, and will be iteratively refined under the guidance of spurious counterexamples. The presented framework is demonstrated by several experiments including a concurrent software system whose server and client processes are derived from openssl-0.9.6c C source codes implementing the SSL protocol.

This paper presents a novel method, namely slicing execution, for model checking C programs with respect to temporal safety properties. The distinguished feature is that it shows a nice approach to the efficient reduction of state space by abstraction and symbolic representation. Slicing execution is founded on an over-approximated semantics of C programs by variable abstraction, and executes symbolically only the relevant statements under abstraction criteria to construct over-approximated finite models of programs, which may be model checked. The variable abstraction criterion begins with a proper initial set of program variables and may be iteratively refined according to spurious counterexamples generated during model checking. In general, the properties to be verified often involve only a few variables in practical programs. In these cases, significant state space reduction, as well as considerable improvement of the scalability, may be achieved. The presented method has been used to verify the initial handshake process of SSL protocol based on the C source code of openssl-0.9.6c. The experiment results confirm that slicing execution is not only practical but also effective.

The Unified Modelling Language (UML) includes a variant of state charts, called state diagrams (SD), for modelling systems with complex interactive behaviour. The official definition of UML specifies the abstract syntax of state diagrams without any formal semantics and hence is unable to perform formal system behaviour analysis. Various attempts have been made to provide such a formal basis for UML state diagrams. Among different attempts, the work reported in [Muan Yong Ng et al. (2003)] is formalizing SD in terms of communicating sequential processes (CSP). In this paper, we present some improvements upon the formalization. The improvements help clarify the semantics of UML SD and make the formalization more complete. Furthermore, we illustrate the use of CSP in reasoning about the equivalence of state diagrams and discuss the benefits of the formalization.

Many approaches exist to decide the order in which classes should be integrated during (integration) testing. Most of them, based on an analysis of class dependencies (for instance described in a UML class diagram) aim at producing a partial order indicating which classes should be tested in sequence and which ones can be tested in parallel. We argue in this article that, thanks to the specifics of such a class test order, it is possible to define an incremental strategy for testing classes that promotes reuse during testing, not only along class inheritance hierarchies.

This paper presents a new approach to generating configuration-oriented executable symbolic test sequences from Extended Finite State Machine (EFSM) models. The information about the values of the context variables and the domain intervals of the input parameters are exploited to guide the derivation of the test sequences. Meanwhile, the transition guards along the test sequences are continually used to reduce the domain intervals of the input parameters. Experiments indicate that this method significantly reduces the EFSM state space to be explored and the number of non-executable symbolic test sequences to be generated. Since parameterized input events are allowed to occur in EFSM cycles, this method is suitable for testing the open reactive systems that interact with the environments via parameterized input events.

SLABS is a formal specification language designed for modular and composable specification of multi-agent systems. This paper reports our attempts to support SLABS at the level of programming languages. A programming language, SLABSp, is presented to support two distinguished mechanisms, namely caste and scenario, in caste-centric methodology of agent-oriented software development. Based on Java platform, the SLABSp has been implemented by compiling the programs into Java with the multi-agent runtime environment.

Although statecharts has gained widespread use as a formalism for modeling reactive real-time systems, testing these systems still confronts some difficulties, of which a major one is the existence of numerous and complex system behaviors. It is extremely difficult to conduct comprehensive and in-depth testing of such real-time systems. This paper presents an approach to property-oriented real-time testing. Necessary real-time extensions are proposed such that the time-enriched statecharts can describe nontrivial timing constraints. The properties to be tested are characterized by a restricted real-time logic. Then the targeted test sequences are derived from the real-time models according to the user-specified properties. Using this approach, testing efforts can be focused on particular properties of the real-time systems and usually only a small portion of the total behaviors needs to be tested.

Scenario has been used to describe agent behaviors in the context of environment situations in the specification languages for agent-based systems, such as SLABS. It becomes an important language facility in the declaration of an agent for specifying its behaviors in its environment. Therefore, towards agent-oriented programming, it is necessary to introduce and implement scenario mechanism in programming languages. This paper reports our attempts to support the language facility from the view of programming languages, and presents an approach to facilitating the scenario mechanism in agent-oriented programming. The basic idea is to extend object-oriented programming language to support agent-oriented programming, where Java is chosen as the base language. Firstly, the language framework of agent-oriented programming, SLABSp is presented, mostly conforming to SLABS, whose syntax is extended based on Java. Scenario mechanism is introduced as the new feature in the programming language. Secondly, the underlying object models are defined to serve as the semantics of the language, where agents are modeled by a couple of objects. A compiler has been built to compile the agent-oriented programs into Java. A running platform has been constructed as the multiagent runtime environment of SLABSp.

Unified Modeling Language (UML) has been widely used in software development. Verifying if an UML model meets the required properties has become a key issue. Model checking is an important technology of automatic formal verification to ensure the correctness of design specifications. An approach of model checking UML statecharts is given in this paper At first, the brief syntax and semantics of UML statecharts are described. Then, the way of how UML statecharts is structurally expressed by extended hierarchical automaton and the labeled transition system are defined. The correctness of operational semantics of UML statecharts can be ensured through finding the maximal non-conflict transition set. For the system with infinite runs, the operational semantics can be mapped to a Buchi automaton and linear temporal logic properties of the system can be verified based on the automata theory of model checking. The paper also presents the method of verifying complex system consist of multiple objects modeled by statecharts and collaboration diagram.

Automatic generation of test data for a given path in a program is an elementary problem in software testing, the difficulty of which lies in how to solve the nonlinear constraint. Gupta et al. (1998) proposed a method, which is referred to as the iterative relaxation method, to address the above problem by linearizing the predicate functions. This paper improves the iterative relaxation method by omitting the constructions of predicate slice and input dependency set, and proves the equivalence of systems of constraints generated by both methods. Since it is not necessary for our method to analyze the dependencies between statements on the path in the course of deriving a system of constraints, our method still works when some statements are only object or executable codes rather than source codes on the path. Therefore, our method can also be used for generating test data for black-box testing and regression testing. We have developed a prototype of a path-wise test data generator whose fundamental algorithm is presented in this paper. The initial experiments with this prototype have shown that our method is practical.

A technique to analyze the temporal properties of real-time systems is presented in this paper. In our framework, the behavior of the system under development, which is modeled in an extension of Statecharts called Statecharts+, is captured by the underlying computational model, Timed Automata. On the basis of the operational semantics defined for arbitrary time domains, we present a formal translation technique to compile the real-time system specification into Timed Automata. Therefore, model checking of real-time properties can be applied to the automatic analysis of real-time systems.>