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 Non-well-separation is a common quality issue in reactive synthesis specifications, where the synthesized system can avoid satisfying its guarantees by preventing the environment from satisfying its assumptions. Kind realizability extends the usual GR(1) by additionally requiring the system to always enable the environment to satisfy its assumptions, thereby addressing this issue, and is expected to replace the usual GR(1) realizability checking. Kind realizability relies on a reduction and a 4-nested fixed-point algorithm, whose runtime typically exceeds that of the usual GR(1) realizability checking algorithm by more than 3 times, creating a significant performance bottleneck in specification development processes that require frequent realizability checks. This paper presents a framework designed to accelerate kind realizability checking, comprising: (1) a multi-level incremental checking framework that sequentially integrates approximate computation with the complete 4FP algorithm, reusing previously computed sound bounds at each stage to eliminate redundant state-space exploration; and (2) two accompanying approximation algorithms with lower asymptotic time complexity, which efficiently compute sound upper and lower bounds of the system winning region. Experiments on benchmarks comprising hundreds of specifications demonstrate significant performance improvements.

Heterogeneous software systems, which often combine closed-source libraries with exported interfaces, embedded assembly, and components in multiple languages, present significant challenges for formal verification. Our prior work, Hetrify, addressed this by converting RISC-V binaries into semantically equivalent C code, making such programs amenable to verification. However, its unified memory model required frequent dynamic computation of stack addresses, which significantly increased the size of the generated logical formulas, along with high memory usage and longer verification times. To address this, we propose memory access specialization, a static analysis and transformation technique that recovers fixed stack offsets during binary conversion to reduce verification overhead. By replacing symbolic stack accesses with fixed-offset memory references, it eliminates dynamic pointer arithmetic and reduces symbolic encoding complexity. This technique is integrated into Hetrify+, an enhanced verification tool for heterogeneous programs. To validate the effectiveness of our approach, we conduct both formal analysis and extensive empirical evaluation. Formal analysis guarantees the correctness of our method. In our evaluation, Hetrify+ demonstrates the same verification accuracy as the original Hetrify on 100 low-level RISC-V assembly programs, achieving up to 2.5× speedup and 4.9× reduction in memory usage. For 30 large-scale heterogeneous programs that include binary-only components, Hetrify+ maintains a 100% success rate, reducing verification time by 1.9× and memory consumption by 1.2×. These results demonstrate that memory access specialization is key to scaling the verification of heterogeneous programs.

Unit testing, as a critical means of ensuring software quality, is often constrained in practice by the high cost and low efficiency of manual test case construction, resulting in limited test coverage and scarcity of unit test cases in real-world projects. Traditional test generation tools can improve coverage but suffer from poor readability and limited generalization. In recent years, large language models (LLMs) have demonstrated strong potential in the field of test generation, owing to their powerful generalization and reasoning capabilities. However, the static nature of training data often causes hallucinations, undermining the reliability of generated tests. To address this, we propose MUATC, a multi-agent unit test generation framework based on LLMs. This work introduces, for the first time in coverage-driven LLM-based test generation, a multi-agent collaborative mechanism that integrates Chain-of-Thought reasoning and Retrieval-Augmented Generation to enhance both the quality and coverage of generated test cases. Additionally, we propose a unit test repair algorithm MTCRA aimed at further improving test coverage. The experimental results show that MUATC achieves 4.8%–5.5% higher coverage than Coverup, with performance gains independent of model architecture and programming languages. Compared with advanced LLM-based coverage enhancement tools such as ChatUniTest, TestPilot and Coverup, MUATC achieves a 12.7% improvement in test coverage on the benchmark dataset provided by ChatUniTest. To demonstrate the superior readability of test cases generated by MUATC, we conducted a readability study via the HumanEval platform. The results indicate that MUATC-generated test cases are significantly more readable than those produced by Pynguin. Therefore, to leverage the high readability of generated test cases, we also develop UnitTestPlat, a user-oriented platform for visualized unit test generation.

Recurrent Neural Networks (RNNs) are widely used in control system due to their dynamic capabilities. However, the control accuracy of RNN-based systems can be compromised by noise interference, and there has been little research on RNN-based control in disturbed multi-agent systems. To address this, we developed an enhanced Distributed RNN (DRNN) structure and proposed a Novel DRNN-based Control Protocol (NDRNN-CP). This enhancement involves introducing a time-delay component, allowing the protocol to adaptively learn noise variation patterns. As a result, the NDRNN-CP effectively resists various periodic noise interferences and achieves more precise control of each agent. Additionally, our optimized activation function ensures that all agents reach consensus within a predefined time. To demonstrate the advantages of NDRNN-CP, we conducted extensive experiments that confirmed its significant improvements in noise signal resistance and convergence performance.

The heterogeneous nature of contemporary software, comprising components like closed-source libraries, embedded assembly snippets, and modules written in multiple programming languages, leads to significant verification challenges. Currently, there are no mature and available methods to effectively address such problems. To bridge this gap, we propose a verification approach capable of effectively verifying heterogeneous programs. This approach is universally applicable. It theoretically supports the verification of any heterogeneous program that can be compiled into binary code, without being constrained by any specific programming language. The approach begins by compiling the entire program or its unverifiable segments into binary format. Under guarantees of semantic equivalence, these binaries are converted into verifiable C code, which can then be verified using existing C verification tools. Based on the RISC-V architecture, we developed the Hetrify tool to implement this verification approach. The tool is supported by rigorous mathematical proofs to ensure operational semantic equivalence between the converted C programs and their original counterparts. To validate our approach, we conducted verification experiments on 130 programs, including 100 assembly programs and 30 large heterogeneous programs with missing critical function source code, demonstrating the effectiveness of our approach.

Large language models (LLMs) have made significant strides in code generation but often struggle with API hallucination issues, especially for the third-party library. Existing approaches attempt to enhance LLMs by incorporating documentation. However, they face three main challenges: the introduction of irrelevant information that distracts the model; reliance solely on documentation that results in discrepancies between API descriptions and practical usage; and the absence of comprehensive error post-processing mechanisms. To address these challenges, we propose THINK11THINK's benchmark and code is available at https://github.com/Leah-Ljx/think., a knowledge injection method that leverages a custom API knowledge database with two phases: pre-execution enhancement and post-execution optimization. The former reduces irrelevant information and integrates multiple knowledge sources, while the latter identifies seven API error types and suggests three heuristic correction strategies. We manually construct a benchmark by collecting and filtering complex API-related tasks from GitHub to evaluate the effectiveness of our method. The experimental results demonstrate that our method can significantly improve the correctness of API usage in the context of LLMs. We reduce the error rate of programs from 61.18% to 16.64% for GPT-3.5 and from 41.49% to 5.58% for GPT-4o across tasks involving different libraries.

Automated evaluation of programming code on online platforms often relies on predefined test cases.However, due to limited test coverage, many programs receive full marks despite violating intended specifications.We present Maveric, a framework that combines large language models (LLMs) with formal verification to more rigorously assess code correctness.Maveric consists of four agents: a template generator that derives formal specifications from problem descriptions, a consistency checker that validates semantic alignment, a code analyzer that detects potential defects and synthesizes counterexamples, and a counterexample validator that formally verifies their validity.We evaluated Maveric on 100 full-score code submissions from 10 real-world programming tasks sourced from a widely used online education platform.Manual review identified 32 with functional defects.Maveric accurately detected 31 of these with no false positives, completing the evaluation of each program in under one minute.In contrast, LLM-only methods detected 25 defects but yielded 6 false positives, while formal verification alone found 23 and suffered frequent timeouts.Importantly, all defects reported by Maveric were supported by verifiable counterexamples, confirming their semantic violations.These results demonstrate Maveric's effectiveness and practicality for automated program evaluation in educational settings.

Code generation has advanced with large language models (LLMs), but LLMs still struggle with complex tasks, especially in competitive programming. These tasks require understanding complex problems, generating correct code that passes numerous test cases, and meeting tight time and memory limits. We observed that there are some critical hints provided by competition platforms, which often point to the most critical information needed to solve the problem, thus guiding participants to accurate solutions. Inspired by these observations, we propose TEACH1, an approach that tutors LLMs in solving competitive programming by combining critical hints with a structured Chain of Thought (CoT). The key insight of TEACH is to employ a domain-specialized hint generator that is fine-tuned on curated data from competitive programming platforms, enabling it to produce concise and targeted algorithmic hints. By integrating these hints into the reasoning process of LLMs, TEACH helps LLMs bridge the gap between complex tasks and solutions. Furthermore, TEACH simulates human problem-solving through a structured CoT that covers problem understanding, analysis, algorithm selection, and coding. We extensively evaluate TEACH on both proprietary (GPT-3.5, GPT-4o, Claude-3.5-Sonnet, Gemini-2.5-Flash) and open-source (DeepSeek-V3) LLMs. TEACH achieves up to 6.56 absolute (17.4% relative) gain in pass@1 on LeetCode, and demonstrates strong generalization to APPS and ASAC, with maximum pass@1 relative improvements of 17.6% and 26.9%, respectively. Furthermore, existing CoT methods with the hints generated from TEACH yield additional gains, demonstrating its compatibility and extensibility across models and prompting strategies.

Dynamic equations provide mathematical frameworks to capture the evolving behavior of systems, which is essential in various fields. While the zeroing neural network (ZNN) is one of the most effective real-time solvers for dynamic equations, it is highly susceptible to noise interference, which reduces the precision and reliability of solutions. Current research struggles to address more complex noise disturbances, particularly complex-valued and random noise. To overcome this limitation, this article introduces a set of self-learning operators with real-time correction ability to counteract noise interference and obtain a new self-learning noise-resistant ZNN (SLNR-ZNN). The operators within the SLNR-ZNN model adaptively learn the physical forms of noise, utilizing the noise’s derivative properties, through continuous system oscillations to enhance noise tolerance and improve the accuracy of dynamic equation resolution. Theoretical analysis and experimental validation show that SLNR-ZNN effectively resolves linear and nonlinear dynamic equations under various types of noise, including constant, harmonic, complex spectral, and Gaussian white noise. Compared to existing ZNN models, SLNR-ZNN achieves comparable convergence rates and simultaneously maintains significantly lower steady-state errors, which are often reduced by nearly an order of magnitude under noise. Furthermore, simulation experiments demonstrate that the SLNR-ZNN-based control protocol achieves state consensus in leader-following multiagent systems and enables trajectory tracking in the UR5 robotic arm with millimeter-level accuracy, even under composite disturbances. These results highlight its practical value and robustness in robotic control applications.

Synthesizing a reactive system fulfilling given requirements is an interesting and challenging problem in the field of formal methods. By using temporal logic as specifications, related results have been well applied in the synthesis of Unmanned Autonomous System (UAS) controllers. But in practice, static and monolithic specifications are usually accompanied with the problem of being unsynthesizable in dynamic and complex environments. To improve the flexibility of controller synthesis, we propose specifications based on criticality levels and corresponding synthesis methods in this paper. When the complete specification is unsynthesizable, according to different synthesis algorithms of initial, transition and goal constraints, the controller that strictly fulfills the critical specifications will be synthesized. The non-critical specifications are used to guide the synthesis process and will be satisfied as much as possible. The proposed methods can improve the adaptability of UAS controller in complex and changeable running environments.

As pre-trained models automate many code intel-ligence tasks, a widely used paradigm is to fine-tune a model on the task dataset for each programming language. A recent study reported that multilingual fine-tuning benefits a range of tasks and models. However, we find that multilingual fine-tuning leads to performance degradation on recent models UniXcoder and CodeT5. To alleviate the potentially catastrophic forgetting issue in multilingual models, we fix all pre-trained model parameters, insert the parameter-efficient structure adapter, and fine-tune it. Updating only 0.6% of the overall parameters compared to full-model fine-tuning for each programming language, adapter tuning yields consistent improvements on code search and sum-marization tasks, achieving state-of-the-art results. In addition, we experimentally show its effectiveness in cross-lingual and low-resource scenarios. Multilingual fine-tuning with 200 samples per programming language approaches the results fine-tuned with the entire dataset on code summarization. Our experiments on three probing tasks show that adapter tuning significantly outperforms full-model fine-tuning and effectively overcomes catastrophic forgetting.

Buffer overflow vulnerabilities are prevalent in software applications, and their automatic detection and exploitation are of great significance. Modern operating systems implement security mitigation to prevent the exploitation of these vulnerabilities, which in turn become obstacles for automatic exploit generation (AEG). Many current AEG solutions do not fully consider security mitigation bypassing and the exploitation of vulnerabilities in special cases, resulting in an inability to accurately assess the exploitability of vulnerabilities in such scenarios. In this paper, we propose a feature-driven buffer overflow vulnerability automatic exploit generation method - FAEG, which uses optimized symbolic execution to search target software for potential buffer overflow vulnerabilities, constructs complete vulnerability models, and then adaptively selects appropriate exploitation techniques based on vulnerability type and features, bypassing system protection and generating effective exploit program.

Code search aims to search for relevant code snippets through queries, which has become an essential requirement to assist programmers in software development. With the availability of large and rapidly growing source code repositories covering various languages, multilingual code search can leverage more training data to learn complementary information across languages. Contrastive learning can naturally understand the similarity between functionally equivalent code across different languages by narrowing the distance between objects with the same function while keeping dissimilar objects further apart. Some works exist addressing monolingual code search problems with contrastive learning, however, they mainly exploit every specific programming language’s textual semantics or syntactic structures for code representation. Due to the high diversity of different languages in terms of syntax, format, and structure, these methods limit the performance of contrastive learning in multilingual training. To bridge this gap, we propose a unified semantic graph representation approach toward multilingual code search called MulCS. Specifically, we first design a general semantic graph construction strategy across different languages by Intermediate Representation (IR). Furthermore, we introduce the contrastive learning module integrated into a gated graph neural network (GGNN) to enhance query-multilingual code matching. The extensive experiments on three representative languages illustrate that our method outperforms state-of-the-art models by 10.7% to 77.5% in terms of MRR on average.

With the rapid increase of public code repositories, developers maintain a great desire to retrieve precise code snippets by using natural language. Despite existing deep learning-based approaches that provide end-to-end solutions (i.e., accept natural language as queries and show related code fragments), the performance of code search in the large-scale repositories is still low in accuracy because of the code representation (e.g., AST) and modeling (e.g., directly fusing features in the attention stage). In this paper, we propose a novel learnable de ep G raph for C ode S earch (called deGraphCS ) to transfer source code into variable-based flow graphs based on an intermediate representation technique, which can model code semantics more precisely than directly processing the code as text or using the syntax tree representation. Furthermore, we propose a graph optimization mechanism to refine the code representation and apply an improved gated graph neural network to model variable-based flow graphs. To evaluate the effectiveness of deGraphCS , we collect a large-scale dataset from GitHub containing 41,152 code snippets written in the C language and reproduce several typical deep code search methods for comparison. The experimental results show that deGraphCS can achieve state-of-the-art performance and accurately retrieve code snippets satisfying the needs of the users.

Static analysis (SA) tools can generate useful static warnings to reveal the problematic code snippets in a software system without dynamically executing the corresponding source code. In the literature, static warnings are of paramount importance because they can easily indicate specific types of software defects in the early stage of a software development process, which accordingly reduces the maintenance costs by a substantial margin. Unfortunately, due to the conservative approximations of such SA tools, a large number of false positive (FP for short) warnings (i.e., they do not indicate real bugs) are generated, making these tools less effective. During the past two decades, therefore, many false positive mitigation (FPM for short) approaches have been proposed so that more accurate and critical warnings can be delivered to developers. This paper offers a detailed survey of research achievements on the topic of FPM. Given the collected 130 surveyed papers, we conduct a comprehensive investigation from five different perspectives. First, we reveal the research trends of this field. Second, we classify the existing FPM approaches into five different types and then present the concrete research progress. Third, we analyze the evaluation system applied to examine the performance of the proposed approaches in terms of studied SA tools, evaluation scenarios, performance indicators, and collected datasets, respectively. Fourth, we summarize the four types of empirical studies relating to SA warnings to exploit the insightful findings that are helpful to reduce FP warnings. Finally, we sum up 10 challenges unresolved in the literature from the aspects of systematicness, effectiveness, completeness, and practicability and outline possible research opportunities based on three emerging techniques in the future.

To speed up the efficiency of software development, the ability to retrieve codes through natural language is fundamental. At present, the approach of code search based on deep learning has been extensively researched and achieved a lot of results. However, these models are much complex and the training relies on artificially extracted features. Different from other deep learning models, we simulate people's reading habit of expanding content first and then refining content when learning new knowledge and propose the concept of Extension-Compression Learning. The model can effectively express the features of code and natural language through Extension Learning and Compression Learning. We evaluate the effect of the approach on the code search task with a small dataset and a large dataset, and the results show that all indicators are better than those of other approaches that embed code and text into a joint vector space.

With the great success of pre-trained models, the pretrain-then-finetune paradigm has been widely adopted on downstream tasks for source code understanding. However, compared to costly training a large-scale model from scratch, how to effectively adapt pre-trained models to a new task has not been fully explored. In this paper, we propose an approach to bridge pre-trained models and code-related tasks. We exploit semantic-preserving transformation to enrich downstream data diversity, and help pre-trained models learn semantic features invariant to these semantically equivalent transformations. Further, we introduce curriculum learning to organize the transformed data in an easy-to-hard manner to fine-tune existing pre-trained models.

Due to the non-deterministic occurring of interrupt service routines, vulnerabilities of interrupt-driven programs, such as data race and atomicity violation, are usually hard to discover. Static analysis is an effective method for vulnerability analysis of interrupt-driven programs. However, existing techniques usually produce a large number of false alarms, which limits the application of static analysis in practice. To achieve high precision in vulnerability analysis of interrupt-driven programs, this paper proposes a program verification enhanced precise analysis method. For each potential vulnerability detected by static analysis, we propose a vulnerability validation approach which employs program verification to further automatically verify its feasibility. We have implemented a prototype of our method on top of CBMC. Experimental results on both an academic benchmark and 24 real-world programs show that our method can successfully identify true vulnerabilities and achieve a high precise analysis.

Many techniques were proposed for detecting software misconfigurations in cloud systems and for diagnosing unintended behavior caused by such misconfigurations. Detection and diagnosis are steps in the right direction: misconfigurations cause many costly failures and severe performance issues. But, we argue that continued focus on detection and diagnosis is symptomatic of a more serious problem: configuration design and implementation are not yet first-class software engineering endeavors in cloud systems. Little is known about how and why developers evolve configuration design and implementation, and the challenges that they face in doing so. This paper presents a source-code level study of the evolution of configuration design and implementation in cloud systems. Our goal is to understand the rationale and developer practices for revising initial configuration design/implementation decisions, especially in response to consequences of misconfigurations. To this end, we studied 1178 configuration-related commits from a 2.5 year version-control history of four large-scale, actively-maintained open-source cloud systems (HDFS, HBase, Spark, and Cassandra). We derive new insights into the software configuration engineering process. Our results motivate new techniques for proactively reducing misconfigurations by improving the configuration design and implementation process in cloud systems. We highlight a number of future research directions.

Code search technique has gradually become a key skill to accelerate software development.However, the current deep learning methods only use the encoded results and ignores the original content of the code.Besides, the feature expression of the code is too single, which makes the model's understanding insufficient.And the last problem is the lack of separate processing of core attributes, which will cause the model to lack differentiated learning of the attributes with different importance.Therefore, we propose a residual network based on Multi-Attention, so that the model can not only retain the original content of the code but also allow the code to perform a large number of combined learning in different aspects to obtain differentiated features.Then we treat three core attributes and specific implementation of the code differently so that the model can pay extra attention to the core attributes.We use 158,201 Java code-comment pairs for training.In our experimental results, our model is 9.5% higher than the existing method on the indicator of MRR and 12% higher on the SuccessRate@1.

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.

The reactive system synthesis for GR(1) fragment of LTL has been widely studied and used in different works. Meanwhile, automatic procedures for generating distributed systems from global behaviors are also thoroughly studied. In this paper, we present a method that automatically constructs cooperative controllers for multi-robot systems from global tasks specified by GR(1). We combine reactive systems synthesis and distributed systems synthesis to solve global task planning problems for multi-robot systems. In short, we specify global tasks for a multi-robot system which consists of several robots, then our algorithm generates individual controllers for robots and also synthesizes a communication strategy. The communication strategy makes robots as a cooperative system through synchronizing them on environment inputs and finally achieves the goal of completing the global tasks. This paper can be used as a cooperative framework for multi-robot systems.

Program synthesis is one of the key research areas in software engineering. Many approaches design domain-specific language to constrain the program space to make the problem tractable. Although these approaches can be effective in certain domains, it is still a challenge to synthesize programs in generic programming languages. Fortunately, the component-based synthesis provides a promising way to generate generic programs from a component library of application programming interfaces (APIs). However, the program space constituted by all the APIs in the library is still very large. Hence, only small programs can be synthesized in practice. In recent years, many approaches of API recommendation have been proposed, which can recommend relevant APIs given some specifications. We think that applying this technique to component-based synthesis is a feasible way to reduce the program space. And we believe that how much support the API recommendation methods can provide to component-based synthesis is also an important criterion in measuring the effectiveness of these methods. In this paper, we investigate 5 state-of-the-art API recommendation methods to study their effectiveness in supporting component-based synthesis. Besides, we propose an approach of API Recommendation via General Search (ARGS). We collect a set of programming tasks and compare our approach with these 5 API recommendation methods on synthesizing these tasks. The experimental results show that the capability of these API recommendation methods is limited in supporting component-based synthesis. On the contrary, ARGS can support component-based synthesis well, which can effectively narrow down the program space and eventually improve the efficiency of program synthesis. The experimental results show that ARGS can help to significantly reduce the synthesis time by 86.1% compared to the original SyPet.

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.

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.

Robotic swarms are usually designed in a bottom-up way, which can make robotic swarms vulnerable to environmental impact. It is particularly true for the widely used control mode of robotic swarms, where it is often the case that neither the correctness of the swarming tasks at the macro level nor the safety of the interaction among agents at the micro level can be guaranteed. To ensure that the behaviors are safe at runtime, it is necessary to take into account the property guard approaches for robotic swarms in uncertain environments. Runtime enforcement is an approach which can guarantee the given properties in system execution and has no scalability issue. Although some runtime enforcement methods have been studied and applied in different domains, they cannot effectively solve the problem of property enforcement on robotic swarm tasks at present. In this paper, an enforcement method is proposed on swarms which should satisfy multi-level properties in uncertain environments. We introduce a macro-micro property enforcing framework with the notion of agent shields and a discrete-time enforcing mechanism called D -time enforcing. To realize this method, a domain specification language and the corresponding enforcer synthesis algorithms are developed. We then apply the approach to enforce the properties of the simulated robotic swarm in the robotflocksim platform. We evaluate and show the effectiveness of the method with experiments on specific unmanned aerial vehicle swarm tasks.

Various robots are playing critical roles in many areas such as industrial manufacturing, disaster rescuing, unmanned vehicle, and science exploration. Because of the uncertain environment, changed resource, or dynamic system structure at runtime, traditional methods such as testing, model checking, and static analysis used in the development stage are not enough to ensure that the executions of robot control software satisfy specified properties. In this paper, we propose a runtime verification approach called Robots Monitor on Multilayer (RMoM) based on robot operating system (ROS) for monitoring whether the running of a robot swarm violates given temporal properties. To monitor robot system in a comprehensive manner over multiple layers, RMoM unifies resource, communication, robot, and swarm properties into a systemic, hierarchical monitoring framework. A discrete-time Metric Temporal Logic (MTL3) RMoM is proposed for specifying properties with timed and parameterized characteristics in robot swarms. Then, the corresponding three-valued semantics is defined for MTL3-RMoM to generate impartial and anticipatory monitors. Moreover, a hierarchical monitoring specification language high-level specification language (HSL)-RMoM and a series of monitor construction algorithms are proposed to automatically generate monitors for MTL3-RMoM properties on ROS platform. The experiments show that the method can automatically generate the monitors for detecting properties of robot swarms.

The synthesis problem is to construct a system fulfilling some specific requirements when interacting with the environment, which is one of the most crucial and challenging tasks in robotics. In comparison to the case of dealing with a single robot, synthesizing of a system constituted with multiple robots is, in general, much more involved. Actually, information is shared among robots in the latter case, and for a fixed robot, when fictively merging the rest ones into its environment, we are confronted with imperfect description of environments. In this article, we present an iterative controller synthesis approach to dealing with multirobot systems. In our model, the behaviors and outputs of one robot can be observed by the other ones, as a part of their inputs. To make our model more flexible, we allow the mechanism of “partial observation,” namely, only a part of outputs can be observed by other robots on some particular sensors. Our synthesis approach is conductive in an iterative manner. By analyzing the dependence among robots, we first try to synthesize controllers for some of them and then extract a set of invariants from the solved part to refine other ones. Repeatedly and iteratively using this way, we may arrive at a complete solution. Meanwhile, in comparison to the monolithic approach, using the iterative manner usually produces a much more compact result, which means that the size of the controller is smaller.

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.

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.

Log messages are widely used in the diagnosis of software failures. Existing studies of failure diagnosis based on log messages tend to use rule-based methods or execution-path-based methods. Rule-based methods generate bug-fixing rules using either human expertise, which is time consuming, or machine learning methods, which may lack the precision of failure diagnosis. To remedy these problems, researchers propose execution-path-based methods that reconstruct execution paths by analyzing source code and run-time logs. These methods, however, may lead to path explosion. To fill this gap, our work focuses on solving the path explosion problem in execution-path-based methods. We assume that run-time logs may have a relationship with their corresponding patches in real-world bug reports. We conduct empirical studies on seven open-source software packages and obtain two findings: (1) 80% of similar bugs have similar patches, and (2) 70% of faulty code is found to lie near the code where the first failure message is printed. Based on these two observations, we design and implement a practical tool NotOnlyLog for bug diagnosis. NotOnlyLog is able to mine the relationships between failure logs and their corresponding patches, in order to reduce both the number and length of uncertain execution paths in bug diagnosis. We evaluate the performance of NotOnlyLog on nine real-world bugs from three large open-source projects. Our experimental results show that, compared with SherLog, NotOnlyLog can achieve a reduction of 86.9% in the number of execution paths.

User Identification with Spatio-Temporal awareness has been attracting much attention from academia. The existing methods not only handle temporal and spatial data separately but also do not consider conflictive check-in records. To tackle these problems, we propose a novel approach that consists of three parts. 1) Measure the similarity of users with a kernel density estimation based method, which handles the spatial and temporal data together; 2) Assign weights to check-in records following the idea of TFIDF, which highlights the discriminative check-in records; 3) Penalize the similarity of users based on the number of conflictive check-in records. The pair-wise users with similarity higher than a predefined threshold are considered to belong to the same individual. Experiments demonstrate the superiority of the proposed approach.

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.

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.

Fuzzing is an important method for binary vulnerability mining.It can analyze binary programs without the source code of the program, which is not easy to do by other technologies.But due to the blindness of input generation, binary fuzzing often falls into traps for a long time when the new mutated inputs cannot generate unexplored paths.In this paper, we propose an efficient and flexible fuzzing framework named Tinker.It defines the Growth Rate of Path Coverage to measure the current state of fuzzing.If the fuzzing falls into low-speed or blocked states, a symbolic analysis procedure is invoked to generate a new input which can help the fuzzing jump out of the trap.In the symbolic analysis procedure, we employ dynamic execution to track the traversed nodes.The untraversed branches are then identified according to the recorded data of AFL.At last, we employ CFG to construct complete paths to these branches and a new input is generated using symbolic execution.Tinker has been implemented and the experiments on DARPA CGC benchmark show that Tinker is more efficient in vulnerability mining than state-of-the-art binary vulnerability mining tools.

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.

Fuzzing is an important method for binary vulnerability mining. It can analyze binary programs without their source codes, which is not easy to do by other technologies. But due to the blindness of input generation, binary fuzzing often falls into traps for a long time when the new mutated inputs cannot generate unexplored paths. In this paper, we propose an efficient and flexible fuzzing framework named Tinker. It defines the growth rate of path coverage to measure the current state of fuzzing. If the fuzzing falls into low-speed or blocked states, a symbolic analysis procedure is invoked to generate a new input which can help the fuzzing jump out of the trap. In the symbolic analysis procedure, we employ dynamic execution to track the traversed nodes. The untraversed branches are then identified according to the recorded data of American Fuzzy Lop (AFL) [M. Zalewski, American Fuzzy Lop (2014), http://lcamtuf.coredump.cx/afl/ ]. At last, we employ control flow graph (CFG) to construct complete paths to these branches and a new input is generated using symbolic execution. Moreover, to expedite the detection of vulnerabilities, we generate inputs which trigger more high-risk system calls first, such that the possibility of finding vulnerabilities can be improved. Tinker has been implemented and the experiments on DARPA CGC benchmark show that Tinker is more efficient in vulnerability mining than state-of-the-art binary vulnerability mining tools.

Misconfigurations have become a major cause of software failures.Most research focuses on misconfiguration diagnosis and troubleshooting, which occur after the misconfigurations have happened.Actually, if we can prevent misconfiguration before software runs, many potential catastrophic failures of systems can be avoided, thus reducing customers' downtime and support costs.In software configuration, we found that most configuration options have specific constraints, which have a strong connection with the configuration option type.If we can check the configuration settings against the inferred type before the software runs, many misconfigurations can be prevented.In this paper, we explore a name-based method called ConfTypeInferer to automatically infer the type of configuration options, which can help users to correctly configure and check settings, thus preventing misconfigurations proactively.We manually studied several popular open-source software projects to investigate the classification and naming conventions of configuration option.Based on these findings, we designed and implemented the ConfTypeInferer.We performed comprehensive experiments to evaluate the effectiveness of our method.

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.

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.

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.

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

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.

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.