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.

In safety verification of hybrid systems, barrier certificates are generated by solving the verification conditions derived from non-negative representations of different types. This paper presents a new computational method, sequential linear programming projection, for directly solving the set of verification conditions represented by the Krivine–Vasilescu–Handelman’s positivstellensatz. The key idea is to decompose it into two successive optimization problems that refine the desired barrier certificate and those undetermined multipliers, respectively, and solve it in an iterative scheme. The most important benefit of the proposed approach lies in that it is much more effective than the LP relaxation method in producing real barrier certificates, and possesses a much lower computational complexity than the popular sum of square relaxation methods, which is demonstrated by the theoretical analysis on complexity and the experiment on a set of examples gathered from the literature.

Barrier certificates generation is widely used in verifying safety properties of hybrid systems because of the relatively low computational complexity it costs. Under sum of squares (SOS) relaxation, the problem of barrier certificate generation is equivalent to that of solving a bilinear matrix inequality (BMI) with a particular type. The paper reveals the special feature of the problem, and adopts it to build a novel computational method. The proposed method introduces a sequential iterative scheme that is able to find analytical solutions, rather than the nonlinear solving procedure to produce numerical solutions used by general BMI solvers and thus is more efficient than them. In addition, different from popular LMI solving based methods, it does not make the verification conditions more conservative, and thus reduces the risk of missing feasible solutions. Benefitting from these two appealing features, it can produce barrier certificates not amenable to existing methods, which is supported by a complexity analysis as well as the experiment on some benchmarks.

Call graph construction serves as a foundational component in Python static analysis and software engineering. However, it faces significant challenges due to the language's unique characteristics. That is, the dynamic typing system, extensive use of third-party libraries, and runtime-dependent behaviors in Python create substantial obstacles for traditional static analysis methods. Although these methods typically achieve high precision, they suffer from low recall, making it difficult to strike a balance between soundness and precision. In this paper, we present InferCG , a hybrid framework that addresses these limitations by combining coarse-grained static analysis with large language model (LLM)–based semantic reasoning. InferCG first constructs a high-recall candidate call set using permissive name- and arity-based matching, and then employs powerful LLMs such as DeepSeek and Qwen to semantically filter implausible edges. This two-stage design balances recall and precision without requiring dynamic execution or extensive type annotations. Experiments on curated open-source Python projects and the DyPyBench benchmark demonstrate that InferCG outperforms state-of-the-art static tools, which achieves up to 13.9% improvement in average recall and a 5.0% gain in average F1 score over PyCG. Moreover, in a real-world vulnerable-function detection scenario, InferCG enables more accurate reachability analysis than dependency-based tools.

Control barrier certificate is an ingenious and practical approach of safety controller synthesis for cyber-physical systems. In this article, we present an approach for synthesizing safety controllers for controlled discrete-time systems subject to safety constraints. We first introduce a new type of $k$ -inductive control barrier certificates ( $k$ -ICBCs), which relaxes the strict nonincreasing condition of general control barrier certificates. Apart from this, we propose a certificate synthesis framework that includes a learner and a verifier. They collaborate continuously to search for safety controllers and their corresponding $k$ -ICBCs simultaneously. The learner obtains neural controllers and candidate $k$ -ICBCs through supervised learning, while the verifier addresses a series of mixed integer linear programming problems to validate the candidate $k$ -ICBCs or provide counterexamples to guide the learner further. Thanks to the less conservatism of $k$ -inductive conditions, safety neural controllers, and $k$ -ICBCs can be easily and quickly obtained. We showcase through benchmark examples that our method is efficient, and $k$ -inductive conditions can improve the effectiveness of control barrier certificate synthesis methods by successfully verifying systems that are challenging to handle with general control barrier certificate conditions.