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.

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.

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.

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.

In the realm of analyzing Rust programs, traditional full-scale analytical approaches are often rendered impractical due to considerable time and performance expenditures.Despite the potential for program slicing technologies to drastically curtail these expenses, the vast majority of existing slicing tools lack compatibility with the Rust language.This study introduces RustPruner, a specialized tool designed for slicing Rust code.RustPruner commences by constructing a goto-style control flow graph (CFG) through rigorous control flow analysis, comprehensively mapping out all feasible execution paths.Subsequently, it leverages a backward slicing algorithm, integrating the outcomes of program dependency analysis and abstract syntax tree (AST) analysis, to generate precise program slices.By innovatively adapting slicing technology to Rust, RustPruner facilitates comprehensive, low-level analysis of Rust's distinctive features.The generated slices undergo rigorous compilation and verification procedures, thereby enhancing the efficiency of the analysis process.The effectiveness of RustPruner has been validated within some crucial system modules of operational operating systems, which significantly improves both the efficiency and accuracy of the verification.

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.

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.

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.

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.

Temporal induction is one of the most popular SAT-based model checking techniques. It consists of two parts, the base case and the induction step. With the search length increment, both parts generate a sequence of SAT problems. This paper focuses on learnt clause replication and reuse in incremental temporal induction. Firstly, with the aid of assumption literals, we present an alternative clause replication scheme, which is much easier to implement than existing works. Secondly, based on our clause replication scheme, we present several clause reuse schemes to maximally explore the learnt clauses and their replications in temporal induction. Based on above ideas, we propose two new incremental temporal induction algorithms. Experimental results on a large number of benchmarks show significant performance improvement of our technique.

Both symbolic model checking and assume-guarantee reasoning aim to circumvent the state explosion problem. Symbolic model checking explores many states simultaneously and reports numerous erroneous traces. Automated assume-guarantee reasoning, on the other hand, infers contextual assumptions by inspecting spurious erroneous traces. One would expect that their integration could further improve the capacity of model checking. Yet examining numerous erroneous traces to deduce contextual assumptions can be very time-consuming. The integration of symbolic model checking and assume-guarantee reasoning is thus far from clear. In this paper, we present a progressive witness analysis algorithm for automated assume-guarantee reasoning to exploit a multitude of traces from BDD-based symbolic model checkers. Our technique successfully integrates symbolic model checking with automated assume-guarantee reasoning by directly inferring BDD's as implicit assumptions. It outperforms monolithic symbolic model checking in four benchmark problems and an industrial case study in experiments.

In many reactive systems, programs run cyclically. In each cycle, they check the current status and handle the business for a single step. The business logic has to be blasted to pieces, which violates the way that people are used to. Cyclic programs are difficult to develop and their reliability is hard to guarantee. To tackle these problems, we propose a model-based formal design flow which is more rigorous and rapid than the V-model. Our method consists of three phases: modeling, verification and code synthesis. In the modeling phase, BIP (Behavior-Interaction-Priority) language, which is expressive and allows flexible modeling, is used as the modeling language. Real-time behavior, that is highly concerned in reactive systems, can be modeled as well. In the verification phase, the system model is translated to timed automata and checked by Uppaal. Verification helps to ensure the correctness of the model. In the code synthesis phase, the software part of the system model is synthesized to cyclic code. We propose an algorithm which can generate high-performance cyclic code from a model which describes the business work-flow. This feature significantly simplifies program development. A set of tools is implemented to support our design flow and they are successfully applied to an industrial case study for a PLC (Programmable Logic Controller) system which is used to control several physical devices in a huge palace.

Large-scale systems are often modeled and verified in a component-based way. BIP (Behavior, Interaction, Priority) is a flexible component-based framework which supports hierarchical design of heterogeneous systems. BIP components interact via connectors in which data can be passed among multiple components. It also support the modeling of time. Due to its expressiveness and flexibility, many real-time systems can be modeled easily in BIP. Verification, however, is not well supported in the current BIP framework. That is a major disadvantage when it is used in a model-driven design flow. To fill this gap, we propose a translation from slightly restricted BIP models to timed automata. Then model checking can be applied to the latter using Uppaal (which is a sophisticated model checker for timed automata). The correctness of translation is proven formally and the translation is implemented as a tool Bip2Uppaal. Three industrial case studies show that our approach is practical and effective.

Temporal induction is a SAT-based model checking technique. We prove that the SAT instances generated by its induction rule can be reduced to the so called Incremental CNFs. A new DPLL procedure is customized for Incremental CNFs, so that the intermediate results in solving previous instances, including the learnt clauses and the search tree, can be reused in solving the next instance. To the best of our knowledge, this is the first result on reusing the search tree in SAT solving of temporal induction. Experimental results on a large number of benchmarks show significant performance gain of our approach.

This paper considers bounded model checking for extended labeled transition systems. Bounded model checking relies on a SAT solver to prove (or disprove) the existence of a counterexample with a bounded length. During the translation of a BMC problem to a SAT problem, much useful information is lost. This paper proposes an algorithm to analyze the transition system model, and then utilize the structure information hidden in the model to refine the decision ordering of variables in SAT solving. The basic idea is to guide the search process of SAT solving by the structure of the transition system. Experiments with this heuristic on real industrial designs show 5-12 times speedup over standard bounded model checking.

Programable logic controllers (PLCs) are complex cyber-physical systems which are widely used in industry. This paper shows the modeling and validation work of a typical PLC control system using the Behavior-Interaction-Priority(BIP) component framework. The gate control system based on PLC is a real industry application. We design general system architecture for this kind of device control system. The control software and hardware of environment are all modeled as BIP components. Their interactions are described by BIP connectors. System requirements are formalized as monitors. Simulation is applied on the system model. We found a couple of design errors in simulation, which help us to improve the dependability of the original systems.

This paper presents a novel efficient satisfiability (SAT) algorithm based on maxterm covering. The satisfiability of a clause set is determined in terms of the number of relative maxterms of the empty clause with respect to the clause set. If the number of relative maxterms is zero, it is unsatisfiable, otherwise satisfiable. A set of synergic heuristic strategies are presented and elaborated. We conduct a number of experiments on 3-SAT and k-SAT problems at the phase transition region, which have been cited as the hardest group of SAT problems. Our experimental results on public benchmarks attest to the fact that, by incorporating our proposed heuristic strategies, our enhanced algorithm runs several orders of magnitude faster than the extension rule algorithm, and it also runs faster than zChaff and MiniSAT for most of k-SAT (k≥3) instances.