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.

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.

Symbolic execution is a powerful technique that can accurately synthesize program inputs for program testing through constraint solving. Applying symbolic execution effectively means that we must solve two searching problems efficiently. One is to search through the many program paths and the other is, given a particular path condition, to search through the numerous variable assignments to identify one satisfying solution. With few exceptions, existing symbolic execution engines treat constraint solvers as black boxes. As a result, the two searches are completely separated, which results in much redundancy (i.e., the same variable assignments may be tried for solving many program paths). Existing attempts on addressing this issue include those approaches based on constrained Horn clauses (in which the whole program is encoded as one constraint) and one preliminary attempt on caching and reusing partial solving results from the constraint solver. In this work, we propose SEC , which systematically computes the reward of concretizing a program path (for symbolic execution) and a variable (for constraint solving) and uses the reward as guide for integrating the two searches. We implemented SEC based on KLEE and evaluated it on a diverse set of programs. The results show that SEC is effective, i.e., achieving 15% more code coverage than the state-of-the-art baseline symbolic execution engines. Furthermore, we show that SEC can be readily combined with a state-of-the-art concolic testing engine to improve its performance

Fuzzing is an efficient automated testing technique for discovering vulnerabilities. It generates and feeds random or pseudo-random data to the target system, aiming to trigger potential bugs or anomalous behaviors that can not be revealed by normal tests designed by system developers. A critical factor in mutation-based fuzzing is seed selection strategy, i.e., how to choose the most promising seed to mutate. Existing seed selection strategies are mostly static and lack the capability to dynamically adjust according to the specific characteristics of different target programs. To address this limitation, we propose a dynamic seed selection strategy based on machine learning techniques. Our method utilizes seed features obtained statically or dynamically to prioritize seeds via a scoring model. The scoring model is trained during the fuzzing process to suit the current target program. Consequently, we can obtain a dynamic seed selection strategy that varies across different programs, and hence enhance the efficiency of fuzzing process. In addition, we use entropy-based power scheduling to improve the performance of fuzzing further. Experimental results on real-world programs demonstrate that our method outperforms the state-of-the-art seed selection method and improves the efficiency of fuzzing especially in the number of discovered unique crashes.

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.

Behavior trees (BTs) are widely adopted in the field of agent control, particularly in robotics, due to their modularity and reactivity. However, constructing a BT that meets the desired expectations is time-consuming and challenging, especially for non-experts. This paper presents BtBot , a multi-modal sketch-based behavior tree synthesis technique. Given a natural language task description and a set of positive and negative examples, BtBot automatically generates a BT program that aligns with the natural language description and meets the requirements of the examples. Inside BtBot , an LLM is employed to understand the task’s natural language description and generate a sketch of the task execution. Then, BtBot searches the sketch to synthesize a candidate BT program consistent with the user-provided positive and negative examples. When the sketch is proven to be incapable of generating the target BT, BtBot provides a multi-step repairing method that modifies the control nodes and structure of the sketch to search for the desired BT. We have implemented BtBot in a prototype and evaluated it on a benchmark of 70 tasks across multiple scenarios. The experimental results indicate that BtBot outperforms the existing BT synthesis techniques in effectiveness and efficiency. In addition, two user studies have been conducted to demonstrate the usefulness of BtBot .

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.

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.

Abstract is a static verifier that can verify the safety properties of C programs. The core of is a program verification framework that synergizes abstract interpretation and symbolic execution in a novel manner. Compared to the individual application of symbolic execution or abstract interpretation, has better efficiency and precision. The implementation of is based on and .

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.

Message-passing interface (MPI) programs are non-deterministic and challenging to ensure correctness. The introduction of one-sided communications makes the problem of non-determinism more severe for MPI programs. This paper reports our in-progress work of symbolic execution for the MPI programs with one-sided communications. Our approach can cover the non-determinism caused by the inputs, one-sided communication, and message- passing operations of MPI programs. The preliminary evaluation's results indicate the promising of our approach.

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.

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.

In scientific computation, developers usually exploit the compiler to improve the performance of floating-point programs. However, many compiler optimizations might affect the floating-point behavior, which can cause numerical variations. This paper proposes an efficient generation method of floating-point inputs for compiler-induced variability. Specifically, we formulate the problem of generating high variability-inducing inputs as a mathematical optimization problem and solve it through input space partition and Markov Chain Monte Carlo (MCMC) sampling. To improve the sampling efficiency, besides the result variation, we utilize the difference between the execution traces of floating-point instructions to guide the search. We have implemented our approach in the tool CIV. Compared to the state-of-the-art method, CIV achieves an average 11x speedup for generating an equivalent or better input to trigger large result variations. Moreover, CIV finds better inputs for 100% programs and has better stability for detecting large result variations. The experimental results demonstrate the effectiveness and efficiency of our approach.

Floating-point programs are challenging for symbolic execution due to the constraint solving problem. To investigate the effectiveness and limitations of the existing methods, we conduct the first empirical study in this paper on five existing symbolic execution methods for floating-point programs. We have implemented the existing methods on the state-of-the-art symbolic execution KLEE and use the real-world representative floatingpoint programs as the benchmarks, which are used to evaluate the existing methods with respect to code coverage and bug finding. The results indicate that the existing methods complement each other in bug finding. Based on the findings of the experimental results, we propose synergizing the existing methods to improve symbolic execution‘s effectiveness. The experimental results demonstrate that our synergic method can detect more bugs.

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.

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.

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.

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.

Constraint solving is one of the challenges for symbolic execution. Modern SMT solvers allow users to customize the internal solving procedure by solving strategies. In this extended abstract, we report our recent progress in synthesizing a program-specific solving strategy for the symbolic execution of a program. We propose a two-stage procedure for symbolic execution. At the first stage, we synthesize a solving strategy by utilizing deep learning techniques. Then, the strategy will be used in the second stage to improve the performance of constraint solving. The preliminary experimental results indicate the promising of our method.

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.

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.

Concolic testing integrates concrete execution (e.g., random testing) and symbolic execution for test case generation. It is shown to be more cost-effective than random testing or symbolic execution sometimes. A concolic testing strategy is a function which decides when to apply random testing or symbolic execution, and if it is the latter case, which program path to symbolically execute. Many heuristics-based strategies have been proposed. It is still an open problem what is the optimal concolic testing strategy. In this work, we make two contributions towards solving this problem. First, we show the optimal strategy can be defined based on the probability of program paths and the cost of constraint solving. The problem of identifying the optimal strategy is then reduced to a model checking problem of Markov Decision Processes with Costs. Secondly, in view of the complexity in identifying the optimal strategy, we design a greedy algorithm for approximating the optimal strategy. We conduct two sets of experiments. One is based on randomly generated models and the other is based on a set of C programs. The results show that existing heuristics have much room to improve and our greedy algorithm often outperforms existing heuristics.

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.

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.

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.

In large-scale cloud computing systems, the growing scale and complexity of component interactions pose great challenges for operators to understand the characteristics of system performance. Performance profiling has long been proved to be an effective approach to performance analysis; however, existing approaches do not consider two new requirements that emerge in cloud computing systems. First, the efficiency of the profiling becomes of critical concern; second, visual analytics should be utilized to make profiling results more readable. To address the above two issues, in this paper, we present P-Tracer, an online performance profiling approach specifically tailored for large-scale cloud computing systems. P-Tracer constructs a specific search engine that adopts a proactive way to process performance logs and generates particular indices for fast queries; furthermore, PTracer provides users with a suite of web-based interfaces to query statistical information of all kinds of services, which helps them quickly and intuitively understand system behavior. The approach has been successfully applied in Alibaba Cloud Computing Inc. to conduct online performance profiling both in production clusters and test clusters. Experience with one real-world case demonstrates that P-Tracer can effectively and efficiently help users conduct performance profiling and localize the primary causes of performance anomalies.

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%).

Modern software applications ranging from enterprise to embedded systems are becoming increasingly complex, and require very high levels of dependability assurance. The most effective means to handle complexity is separation of concerns and incremental development, and assurance of dependability requires formal methods. We report here our experience on these issues in an application of a formal calculus, rCOS, to a component-based design of the point of sale system (POS). We demonstrate the possibility in scaling-up correctness by design and discuss how rCOS may be integrated with current and emerging software engineering tools.

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