Abstract Safe controller synthesis with formal guarantees is widely employed in safety-critical systems. However, existing controller synthesis methods are subject to significant limitations in scalability and efficiency. This paper presents a novel controller incremental synthesis framework guided by barrier certificates (BCs), thereby generating a safe controller with BC verification. To enhance verification efficiency, we construct a learning-enabled polynomial BC combined with efficient post-verification, which is transformed into smaller-scale linear Programming (LP) subproblems for feasibility determination. Furthermore, we have implemented a tool called ISafeC and evaluated its performance over a set of benchmark examples. The comparative experimental results demonstrate the effectiveness and efficiency of our approach.

Safe controller synthesis is crucial for safety-critical applications. This paper presents a novel reinforcement learning approach to synthesize safe controllers for NN-controlled systems. The core idea leverages an iterative scheme that combines controller learning with neural barrier certificate (BC) verification, ultimately producing a provably safe deep neural network (DNN) controller with formal safety guarantees. The process begins by pre-training a well-performing DNN controller as an “oracle” via deep reinforcement learning (DRL). To formally verify the safety properties of the closed-loop system under the base controller, we devise a formal verification procedure that approximates the DNN controller using polynomial inclusion, followed by synthesizing neural BCs via sum-of-squares (SOS) relaxation. In cases where the base controller is insufficient to yield a real BC, the current spurious BC is incorporated as an additional penalty term to reshape the RL reward function, guiding the iterative refinement for new controllers. We implement an automated tool, NBCRL, and experimental results demonstrate the benefits of our method in terms of efficiency and scalability even for a nonlinear system with dimension up to 12.

Polynomial inequality proving is fundamental to many mathematical disciplines and finds wide applications in diverse fields. Current traditional algebraic methods are based on searching for a polynomial positive definite representation over a set of basis. However, these methods are limited by truncation degree. To address this issue, this paper proposes an approach based on reinforcement learning to find a Krivine-basis representation for proving polynomial inequalities. Specifically, we formulate the inequality proving problem as a linear programming (LP) problem and encode it as a basis selection problem using reinforcement learning (RL), achieving a non-negative Krivine basis. Moreover, a fast multivariate polynomial multiplication method based on Fast Fourier Transform (FFT) is employed to enhance the efficiency of action space search. Furthermore, we have implemented a tool called APPIRL (Automated Proof of Polynomial Inequalities via Reinforcement Learning). Experimental evaluation on benchmark problems demonstrates the feasibility and effectiveness of our approach. In addition, APPIRL has been successfully applied to solve the maximum stable set problem.

The design of controllers for safety-critical systems is an important research issue. Especially, the generation of controllers with formal safety guarantees is a challenging problem. Recently, for safety objectives of various system control tasks, machine learning technologies have been used to achieve ideal training and simulation performance, but formal guarantees are still lacking. This paper takes advantages of learning technology to assist safe controller synthesis with formal guarantees. On the one hand, the generation of verifiable safe controllers is aided by reinforcement learning; on the other hand, a set of barrier certificates (BC), i.e. a vector BC, is synthesized with the aid of deep learning to certify the safety of synthesized controllers. Vector BCs are more expressive than the conventional single BCs for safety verification. Compared with the existing work on vector BC generation, our method has two advantages: first, our method verifies a learned candidate vector BC, rather than directly generating a verified one, and thus has low computational complexity; second, the existing method has made relaxations to the non-convex vector BC constraints, which reduced the feasible region of solutions, while our method can deal with the original constraints. Furthermore, experiments fully demonstrate the effectiveness of our method on a series of benchmarks.

User Interface (UI) testing is crucial for quality assurance of industrial mobile applications, and yet it remains labor-intensive and challenging to automate effectively. Recent advances in Vision-Language Models (VLMs) present a promising solution for automating GUI testing by mapping natural language instructions to pixel-level actions, significantly reducing the manual effort required for writing test scripts and even designing test cases. While numerous VLMs have been proposed and evaluated for GUI testing, they often fail to meet two critical industrial requirements: (1) effectiveness when handling complex, multi-step workflows in industrial applications, and (2) efficiency for large-scale, high-frequency testing environments typical in industrial settings. Toward addressing the preceding industrial requirements, in this paper, we report our experiences in developing and deploying RePeek, a novel approach employing a unified three-stage pipeline for both training and inference, enables a VLM to explicitly detect and reason over discrete GUI elements, thereby overcoming the limitations of pixel-based reasoning for both efficiency and effectiveness improvements. In the first stage, RePeek integrates a lightweight UI-element detector named OmniParser to decompose UI screenshots into a structured element list. In the second stage, RePeek adopts the vision encoder of the VLM to generate the embedding for each element. In the third stage, RePeek fuses these element embeddings with the textual instruction to reason and perform classification directly on the UI elements, empowering efficient small models to achieve superior performance against expensive large models. Comprehensive evaluations on public benchmarks and deployment at WeChat show that RePeek consistently achieves superior accuracy and efficiency compared to state-of-the-art VLMs. Specifically, RePeek enables a fine-tuned Qwen2.5-VL-3B model to outperform a 72B model with 75% less training data, validating the effectiveness of incorporating domain knowledge into VLM-based GUI testing. We conclude by summarizing three key lessons from developing and deploying RePeek, offering insights for both researchers and practitioners working on industrial-strength UI testing.

Controller synthesis for nonlinear systems is an important research issue. Deep Neural Network (DNN) control policies obtained through reinforcement learning (RL), though exhibiting good performance in simulations, cannot be applied to safety-critical systems for lack of formal guarantee. To address this, this paper considers fully utilizing the advantages of RL for complex control tasks to obtain a well-performing DNN controller. Then, using PAC (Probably Approximately Correct) techniques, a polynomial surrogate controller with probabilistically controllable approximation error is obtained. Finally, the safety of the control system under the designed polynomial controller is verified using barrier certificate generation. Experiments demonstrate the effectiveness of our method in generating controllers with safety guarantees for systems with high dimensions and degrees.

There is a pressing need to ensure the safety of closed-loop systems with neural network controllers, as they are often incorporated into safety-critical applications. To address this issue, we propose a novel approach for generating barrier certificates, which combines counterexample-guided learning with efficient Sum-Of-Squares (SOS) based verification. By leveraging barrier certificate candidates obtained from the learning phase, our proposed method offers an efficient verification procedure that solves three Linear Matrix Inequality (LMI) constraint feasibility testing problems, instead of relying on an SMT solver to verify the barrier certificate conditions. We conduct comparison experiments on a set of benchmarks, demonstrating the advantages of our method in terms of efficiency and scalability, which enable effective verification of high-dimensional systems.

Research on misinformation detection has primarily focused either on furthering Artificial Intelligence (AI) for automated detection or on studying humans' ability to deliver an effective crowdsourced solution. Each of these directions however shows different benefits. This motivates our work to study hybrid human-AI approaches jointly leveraging the potential of large language models and crowdsourcing, which is understudied to date. We propose novel combination strategies Model First, Worker First, and Meta Vote, which we evaluate along with baseline methods such as mean, median, hard- and soft-voting. Using 120 statements from the PolitiFact dataset, and a combination of state-of-the-art AI models and crowdsourced assessments, we evaluate the effectiveness of these combination strategies. Results suggest that the effectiveness varies with scales granularity, and that combining AI and human judgments enhances truthfulness assessments' effectiveness and robustness.

Bayesian neural networks (BNNs) retain NN structures with a probability distribution placed over their weights. With the introduced uncertainties and redundancies, BNNs are proper choices of robust controllers for safety-critical control systems. This paper considers the problem of verifying the safety of nonlinear closed-loop systems with BNN controllers over unbounded-time horizon. In essence, we compute a safe weight set such that as long as the BNN controller is always applied with weights sampled from the safe weight set, the controlled system is guaranteed to be safe. We propose a novel two-phase method for the safe weight set computation. First, we construct a reference safe control set that constraints the control inputs, through polynomial approximation to the BNN controller followed by polynomial-optimization-based barrier certificate generation. Then, the computation of safe weight set is reduced to a range inclusion problem of the BNN on the system domain w.r.t. the safe control set, which can be solved incrementally and the set of safe weights can be extracted. Compared with the existing method based on invariant learning and mixed-integer linear programming, we could compute safe weight sets with larger radii on a series of linear benchmarks. Moreover, experiments on a series of widely used nonlinear control tasks show that our method can synthesize large safe weight sets with probability measure as high as 95% even for a large-scale system of dimension 7.

Abstract There is a pressing need for learning controllers to endow systems with properties of safety and goal-reaching, which are crucial for many safety-critical systems. Reinforcement learning (RL) has been deployed successfully to synthesize controllers from user-defined reward functions encoding desired system requirements. However, it remains a significant challenge in synthesizing provably correct controllers with safety and goal-reaching requirements. To address this issue, we try to design a special hybrid polynomial-DNN controller which is easy to verify without losing its expressiveness and flexibility. This paper proposes a novel method to synthesize such a hybrid controller based on RL, low-degree polynomial fitting and knowledge distillation. It also gives a computational approach, by building and solving a constrained optimization problem coming from verification conditions to produce barrier certificates and Lyapunov-like functions, which can guarantee every trajectory from the initial set of the system with the resulted controller satisfies the given safety and goal-reaching requirements. We evaluate the proposed hybrid controller synthesis method on a set of benchmark examples, including several high-dimensional systems. The results validate the effectiveness and applicability of our approach.

There is a pressing need to synthesize provable safety controllers for nonlinear systems as they are embedded in many safety-critical applications. In this paper, we propose a safe Meta Reinforcement Learning (Meta-RL) approach to synthesize deep neural network (DNN) controllers for nonlinear systems subject to safety constraints. Our approach incorporates two phases: Meta-RL for training the controller network, and formal safety verification based on polynomial optimization solving. In the training phase, we provide a training framework which pre-trains a unified meta-initial controller for control systems by meta-learning. An important benefit of the proposed Meta-RL approach lies in that it is much more effective and succeeds in more controller training tasks compared with existing typical RL methods, e.g., Deep Deterministic Policy Gradient (DDPG). To formally verify the safety properties of the closed-loop system with the learned controller, we develop a verification procedure by using polynomial inclusion computation in combination with barrier certificate generation. Experiments on a set of benchmarks, including systems with dimension up to 12, demonstrate the effectiveness and applicability of our method.

This paper presents a novel approach to safety verification based on neural barrier certificates synthesis for continuous dynamical systems. We construct the synthesis framework as an inductive loop between a Learner and a Verifier based on barrier certificate learning and counterexample guidance. Compared with the counterexample-guided verification method based on the SMT solver, we design and learn neural barrier functions with special structure, and use the special form to convert the counterexample generation into a polynomial optimization problem for obtaining the optimal counterexample. In the verification phase, the task of identifying the real barrier certificate can be tackled by solving the Linear Matrix Inequalities (LMI) feasibility problem, which is efficient and makes the proposed method formally sound. The experimental results demonstrate that our approach is more effective and practical than the traditional SOS-based barrier certificates synthesis and the state-of-the-art neural barrier certificates learning approach.

Abstract In this paper, we propose a safe reinforcement learning approach to synthesize deep neural network (DNN) controllers for nonlinear systems subject to safety constraints. The proposed approach employs an iterative scheme where alearnerand averifierinteract to synthesize safe DNN controllers. Thelearnertrains a DNN controller via deep reinforcement learning, and theverifiercertifies the learned controller through computing a maximal safe initial region and its corresponding barrier certificate, based on polynomial abstraction and bilinear matrix inequalities solving. Compared with the existing verification-in-the-loop synthesis methods, our iterative framework is a sequential synthesis scheme of controllers and barrier certificates, which can learn safe controllers with adaptive barrier certificates rather than user-defined ones. We implement the tool SRLBC and evaluate its performance over a set of benchmark examples. The experimental results demonstrate that our approach efficiently synthesizes safe DNN controllers even for a nonlinear system with dimension up to 12.

GUI testing is an essential part of regression testing for Android apps. For regression GUI testing to remain effective, it is important that obsolete GUI test scripts get repaired after the app has evolved. In this paper, we propose a novel approach named GUIDER to automated repair of GUI test scripts for Android apps. The key novelty of the approach lies in the utilization of both structural and visual information of widgets on app GUIs to better understand what widgets of the base version app become in the updated version. A supporting tool has been implemented for the approach. Experiments conducted on the popular messaging and social media app WeChat show that GUIDER is both effective and efficient. Repairs produced by GUIDER enabled 88.8% and 54.9% more test actions to run correctly than those produced by existing approaches to GUI test repair that rely solely on visual or structural information of app GUIs.

Abstract We provide a new approach to synthesize controllers for nonlinear continuous dynamical systems with control against safety properties. The controllers are based on neural networks (NNs). To certify the safety property we utilize barrier functions, which are represented by NNs as well. We train the controller-NN and barrier-NN simultaneously, achieving a verification-in-the-loop synthesis. We provide a prototype tool nncontroller with a number of case studies. The experiment results confirm the feasibility and efficacy of our approach.

This paper presents an approach of safety verification based on neural networks for continuous dynamical systems which are modeled as a system of ordinary differential equations. We adopt the deductive verification methods based on barrier certificates. These are functions over the states of the dynamical system with certain constraints the existence of which entails the safety of the system under consideration. We propose to represent the barrier function by neural networks and provide a comprehensive synthesis framework. In particular, we devise a new type of activation functions, i.e., Bent-ReLU, for the neural networks; we provide sampling based approaches to generate training sets and formulate the loss functions for neural network training which can capture the essence of barrier certificate; we also present practical methods to check a learnt candidate barrier certificate against the criteria of barrier certificates as a formal guarantee. We implement our approaches via proof-of-concept experiments with encouraging results.

For large industrial applications, system test cases are still often described in natural language (NL), and their number can reach thousands. Test automation is to automatically execute the test cases. Achieving test automation typically requires substantial manual effort for creating executable test scripts from these NL test cases. In particular, given that each NL test case consists of a sequence of NL test steps, testers first implement a test API method for each test step and then write a test script for invoking these test API methods sequentially for test automation. Across different test cases, multiple test steps can share semantic similarities, supposedly mapped to the same API method. However, due to numerous test steps in various NL forms under manual inspection, testers may not realize those semantically similar test steps and thus waste effort to implement duplicate test API methods for them. To address this issue, in this paper, we propose a new approach based on natural language processing to cluster similar NL test steps together such that the test steps in each cluster can be mapped to the same test API method. Our approach includes domain-specific word embedding training along with measurement based on Relaxed Word Mover’sDistance to analyze the similarity of test steps. Our approach also includes a technique to combine hierarchical agglomerative clustering and K-means clustering post-refinement to derive high-quality and manually-adjustable clustering results. The evaluation results of our approach on a large industrial mobile app, WeChat, show that our approach can cluster the test steps with high accuracy, substantially reducing the number of clusters and thus reducing the downstream manual effort. In particular, compared with the baseline approach, our approach achieves 79.8% improvement on cluster quality, reducing 65.9% number of clusters, i.e., the number of test API methods to be implemented.

Benefit from less computational difficulty, barrier certificate based method has attracted much attention in safety verification of hybrid systems. Barrier certificates are inherent existences of a hybrid system and may have different types. A set of well-defined verification conditions is a prerequisite for successfully identifying barrier certificates of a specific type. Therefore, how to define verification conditions that can identify barrier certificates invisible to existing conditions becomes an essential problem in barrier certificate based verification. This paper proposes a set of verification conditions that helps to construct a new type of barrier certificate, namely, the Darboux-type barrier certificate made of Darboux polynomial. The proposed verification conditions provide powerful aids in non-linear hybrid system verification as the Darboux-type barrier certificates can verify systems that may not be settled by existing verification conditions.

Given the ever increasing number of research tools to automatically generate inputs to test Android applications (or simply apps), researchers recently asked the question "Are we there yet?" (in terms of the practicality of the tools). By conducting an empirical study of the various tools, the researchers found that Monkey (the most widely used tool of this category in industrial practices) outperformed all of the research tools that they studied. In this paper, we present two significant extensions of that study. First, we conduct the first industrial case study of applying Monkey against WeChat, a popular messenger app with over 762 million monthly active users, and report the empirical findings on Monkey's limitations in an industrial setting. Second, we develop a new approach to address major limitations of Monkey and accomplish substantial code-coverage improvements over Monkey, along with empirical insights for future enhancements to both Monkey and our approach.