Abstract:Current quantum programs are usually represented as quantum circuits,including various quantum gates.If the program contains gates that are represented as unitary matrices,these gates need to be transformed into quantum circuits composed of basic gates.However,current synthesis methods may generate inferior circuits with thousands of gates,which leads to failure when deploying to real-world quantum hardware.Moreover,the process to minimize the number of gate takes weeks or even months when the number of qubits goes to 8.In this work,we propose Fast-USYN that enables fast synthesis from unitary to high-quality quantum circuits.We first introduce an iterative approach that approximates the target unitary by inserting circuit blocks.The minimization of gates is achieved by a look-ahead strategy with a rewarding mechanism to reduce redundant gates.In the acceleration of unitary synthesis,instead of exhaustively enumerating tremendous candidates,we construct the search space by depicting the closure of each candidate.Furthermore,to reduce the overhead of searching the optimal gate parameters,we pack the selected candidates with the target unitary into a uniform circuit so that we can quickly obtain the approximation distance by calculating its expectation on the ground state.Experiments show that Fast-USYN achieves 1.6-2.7 times gate reduction and 3.7-20.6 times speedup for 5-qubit to 8-qubit synthesis,compared to QuCT^[1] and QFAST^[9].

Abstract:Constraint solving is a fundamental approach for verifying deep neural networks (DNNs). In the field of AI safety, DNNs often undergo modifications in their structure and parameters for purposes such as repair or attack. In such scenarios, we propose the problem of incremental DNN verification, which aims to determine whether a safety property still holds after the DNN has been modified. To address this problem, we present an incremental satisfiability modulo theory (SMT) algorithm based on the Reluplex framework. Our algorithm, called DeepInc, simulates the key features of the configurations that infer the verification results of the old solving procedure . It heuristically checks whether the proofs remain valid for the modified DNN. Experimental results demonstrate that DeepInc outperforms Marabou in efficiency in most cases. Moreover, for cases where the property is violated both before and after modification, DeepInc achieves significantly faster acceleration, even when compared to the state-of-the-art verifier α, β-CROWN.

Abstract:The single-sphere driven balance robot is an omnidirectional mobile robot, whose flexibility is especially apparent in narrow or complex environments. During the design of the kinematics and dynamics of this type of robot, it is important to ensure the correctness of the model. Traditional methods based on testing and simulation may not exhaust all system states, and thus might fail to identify certain design flaws or potential safety risks. To ensure that the single-sphere driven balance robot meets the correctness and safety verification requirements of safety-critical robots, this paper used the HOL Light theorem prover to construct a formal model of the kinematics and dynamics of this type of robot. The model is based on theorem libraries such as the real analysis library, the matrix analysis library, the robot kinematics and dynamics library, and carries out a higher-order logic derivation and proof.

Abstract:Meta-Interpretive Learning (MIL) is a method of Inductive Logic Programming (ILP), aiming to learn a program from a set of examples, metarules, and other background knowledge. MIL adopts a depth-first and failure-driven strategy to search proper clauses in the program space for generating programs. As a matter of fact, this mechanism inevitably raises the problem of repeated proof for the same goals. In this paper, we propose a pruning strategy that leverages the built-in database mechanism of Prolog to store the failed goals and their corresponding error information, effectively avoiding redundant proof processes. Subsequently, this accumulated error information can serve as guidance to assist the MIL system in optimizing and adjusting its learning process in the future. We prove the correctness of the pruning algorithm and calculate the reduced proportion of the program space in theory. We apply the proposed approach to two existing MIL systems Metagol and Metagol_AI, resulting in two new MIL systems Metagol_F and Metagol_{AI_F}. Empirical results on four different tasks show that the proposed strategy can significantly reduce the time consumption for learning the same programs.

Abstract:The operating system serves as the foundational platform for software, and the security of its kernel is often of significant importance. Rust, a memory-safe language that has been gradually gaining popularity, incorporates safety mechanisms such as lifetimes, ownership, borrowing checks, and RAII. Building kernels using Rust has become a prominent area of research. However, systems constructed with Rust often contain some unsafe code segments, preventing the language from offering comprehensive guarantees of safety at the language level. Therefore, verifying these unsafe code segments is crucial for ensuring the correctness and reliability of Rust-based kernels. This paper proposes a method for combining the safe and unsafe code segments, called GhostFunc, to verify a microkernel built with Rust. The method applies different levels of abstraction to the two types of code segments and uses GhostFunc for the combination verification. Focusing on the task management and scheduling module, this paper formalizes unsafe code segments such as Arc<T> using λ_Rust and presents the formal implementation of GhostFunc. A verification example of this method is also provided. All verification work is based on theorem proving, and correctness is validated in Coq using the Iris separation logic framework.

Abstract:Extreme scenarios in autonomous driving, as well as unpredictable human behaviors, have become key factors restricting the development of Autonomous Driving Systems (ADS). Therefore, effectively generating safety-critical scenarios is crucial for enhancing the safety of ADS. Existing methods for generating autonomous driving scenarios mainly rely on substantial road-collecting and employ data-driven approaches combined with scenario generalization techniques, These methods are time-consuming, labor-intensive, and costly, making it difficult to effectively generate edge cases. In contrast, model-driven scenario modeling methods can construct logical scenario models to encapsulate complex scene features and effectively generate safety-critical scenarios. However, The challenging issue it faces is how to design a domain-knowledge-based visual scenario modeling language that supports the abstract modeling of complex driving scenarios and further effectively explores edge-critical scenarios To address these issues, this paper proposes an approach for scenario modeling with SML4ADS2.0 and edge-critical scenario generation for autonomous driving system. This method utilizes ontology modeling of scenarios within the ADS domain, combining formal quantitative evaluation with importance sampling to generate edge-critical scenarios. First, we propose a model-driven scenario modeling method based on SML4ADS2.0, designing a Scenario Modeling Language for Autonomous Driving System (SML4ADS2.0) to construct models of autonomous driving scenarios. Secondly, we implement the conversion of scenario models to Stochastic Hybrid Automata (SHA) through model transformation rules and use the model checking tool UPPAAL-SMC for quantitative evaluation and analysis of the scenario models. Subsequently, we employ importance sampling techniques to rapidly detect edge scenarios within the scenario space, effectively generating specific edge-critical scenarios from logical scenes. Finally, we demonstrate the method with case studies involving typical scenarios such as lane changes and overtaking. Experimental results indicate that this approach can effectively model scenarios and address the generation of safety-critical scenarios for ADS.

Abstract:Dynamic order statistic tree structures are a type of data structure that integrates the features of dynamic sets, order statistics, and search tree structures, supporting efficient data retrieval operations. These structures are widely used in fields like database systems, memory management, and file management. However, current research primarily focuses on structural invariants, such as balance, while neglecting discussions on functional correctness. Additionally, existing research methods mainly involve manual derivation or interactive mechanized verification for specific algorithms, lacking mature and reliable general verification patterns and having a low level of automation. To address this, an Isabelle-based functional modeling and automated verification framework for dynamic order statistic search tree structures was designed, establishing a verified general lemma library to reduce the time and cost of code verification for developers. Using this functional modeling framework, unbalanced binary search trees, balanced binary search trees (exemplified by red-black trees), and balanced multi-way search trees (exemplified by 2-3 trees) were selected as instantiated cases for demonstration. With the help of the automated verification framework, multiple instantiated cases can be automatically verified by simply using induction and calling the auto method once or the try command, providing a reference for automated verification of functional and structural correctness in complex data structure algorithms.

Abstract:The synchronous dataflow language Lustre is commonly used in the development of safety-critical systems. However, existing official code generators and the SCADE KCG code generator have neither been formally verified nor are they transparent to users. In recent years, translation validation methods that indirectly verify the correctness of compilers by proving the equivalence of source and target codes have been shown to be successful. This paper proposes a trusted compilation method for the Lustre language, based on a pushdown automaton compilation approach and a semantic consistency verification method. It successfully implements a trusted compiler from Lustre to C and rigorously proves the correctness of the translation process using Isabelle.

Abstract:Operating system (OS) kernels are the basis of designing safety-critical software systems. The correct running of any computer systems relies on the correctness of the underlying OS kernels, therefore, it is highly desirable to verify the correctness of OS kernels formally. However, the behavior such as multi-task concurrency, data sharing and race that exist in OS, brings great challenge to the verification of OS kernels. Recently, the theorem proving based methods have been applied for the formal verification of OS functionality modules, and achieved some successful applications. OS kernel capability-based access control module provides a fine-grained access control, designed to prevent unauthorized users from accessing system kernel resources and services. In the implementation of the capability-based access control, the capability spaces of all tasks form a set of tree structures, and at the same time each capability node contains nested complex data structures, plus the widespread operations in capability functions including access, modification, and (recursive) deletion to capability space, make the formal verification of capability-based access control more difficult compared to other OS modules. In this paper, based on concurrent separation logic with refinement CSL-R, we have verified the functional correctness of capability-based access control of an OS kernel in aerospace embedded field, by proving the refinement between capability API functions and their abstract specification. We first formally define the capability data structure, based on which we define the global capability invariant to keep the consistency of the capability spaces; then, we define the pre/post-conditions for internal functions and the abstract specification for API functions that reflect their functional correctness; and finally, we prove the refinement between the C implementation for API functions and their abstract specification. All the above definitions and verification are formalized in Coq theorem prover. During verification, we found errors for the C implementation, which have been confirmed and modified by the designer of the OS kernel.

Abstract:Cyber-Physical Systems (CPS) find extensive applications in safety-critical domains, making it crucial to ensure their safety. Formal verification is a powerful technique for proving system safety, but its application in complex, real-world CPS remains challenging. Falsification is therefore proposed, which aims to prove the unsafety of a system by identifying counterexample system behaviors that violate given safety properties. Existing path-oriented CPS falsification methods employ divide-and-conquer strategies, exploring system behavior along system paths, and can discover unsafe behaviors effectively. However, in large-scale CPSs, these methods face the serious challenge of path explosion. As the number of discrete system modes increases, the number of paths grows exponentially, leading to a notable decrease in falsification efficiency and performance. To mitigate the path explosion problem during path-oriented falsification, this paper proposes two techniques based on the system model and specification: path filtering and dynamic path selection. Firstly, we introduce a specification-driven path filtering technique that rapidly filters out paths unlikely to contain unsafe behaviors by analyzing the syntax tree of system specifications and the constraints on behaviors along each path. Secondly, we employ a multi-armed bandit algorithm to dynamically select paths to be falsified during the falsification process, adaptively adjusting computational resources allocated to explore different paths to maximize performance. Experimental results on a series of classical benchmarks show that our techniques significantly alleviate the path explosion issue and improve CPS falsification performance, leading to a twofold increase in the success rate of identifying unsafe system behaviors.

Abstract:As an emerging safe system programming language, Rust provides guarantees for memory safety and concurrency safety with its innovative ownership model and borrowing mechanism. Although Rust focuses on safety, existing works has revealed numerous safety challenges it still faces. Formal verification is a method based on rigorous mathematical foundations. It offers strong assurance for enhancing Rust's security. By formalizing precise and clear semantic models, it is possible to prove that programs adhering to Rust's typing rules meet safety requirements. Automated Rust verification tools can assist users in ensuring the safety and correctness of Rust programs. This survey provides a comprehensive and systematic analysis of Rust formal verification. First, it introduces the core semantics and complex features of Rust, and discusses research and verification work on Rust's formal semantics afterwards, highlighting the potential of Rust's type system in formal verification. Second, the paper systematically compares the abilities, language features supported, underlying technologies, and applicable scenarios of different Rust automated verification tools. It is significant for guiding the selection and integration of tools in the actual development process of Rust projects. Additionally, this paper summarizes verified Rust systems, demonstrating the remarkable effectiveness of formal verification in ensuring program correctness, and provides tool selection recommendations for users. Finally, this paper concludes by discussing the current challenges in the field and pointing out directions for future research, including the verification of unsafe Rust code, concurrent code verification, trustworthy compilation, and formal verification driven by large models. This paper aims to provide a solid security foundation for the Rust community and promote the application of formal verification in Rust development.

Abstract:With the rapid development of Intelligent Cyber-Physical Systems (ICPS), intelligent technologies are increasingly being applied in intelligent components such as perception, decision-making, and control. Among these, deep reinforcement learning (DRL) has been widely used in the control components of ICPS due to its efficiency in handling complex dynamic environments. However, the openness of the operating environment and the complexity of ICPS require DRL to explore a highly dynamic state space during the learning process, which can lead to inefficiencies and inadequate generalization in decision-making. A common solution to this problem is to abstract a large-scale fine-grained Markov Decision Process (MDP) into a smaller-scale coarse-grained MDP, thereby simplifying the model’s computational complexity and improving the solution efficiency. However, these methods have yet to address how to ensure the semantic consistency between the temporal-spatial semantic information of the original states, the clustered abstract system space, and the real system space. To solve the above problems, this paper proposes a causal temporal-spatial semantic-based abstraction modeling method for deep reinforcement learning. First, causal temporal-spatial semantics reflecting the distribution of value changes over time and space are introduced, and based on this, a two-stage semantic abstraction is performed on the states to construct an abstract MDP model for the deep reinforcement learning process. Next, abstraction optimization techniques are employed to refine the abstract model, reducing the semantic errors between the abstract states and the corresponding specific states. Finally, extensive experiments were conducted using cases such as lane-keeping, adaptive cruise control, and intersection crossing, and the model was evaluated and analyzed with the PRISM verifier. The results demonstrate that our proposed abstraction modeling technique performs well in terms of the model’s abstraction capability, accuracy, and semantic equivalence.