In the robustness verification of neural networks, formal methods have been used to give deterministic guarantees for neural networks. However, recent studies have found that the verification method of single-neuron relaxation in this field has an inherent convex barrier that affects its verification capability. To address this problem, we propose a new verification method by combining dual-neuron relaxation and linear programming. This method captures the dependencies between different neurons in the same hidden layer by adding a two-neuron joint constraint to the linear programming model, thus overcoming the convex barrier problem caused by relaxation for only a single neuron. Our method avoids the combination of exponential inequality constraints and can be computed in polynomial time. Experimental results show that we can obtain tighter bounds and achieve more accurate verification than single-neuron relaxation methods.

The verification techniques based on formal methods can provide deterministic guarantees for the robustness of Deep Neural Networks(DNNS). However, the enormous scale of DNNS makes the application of such methods in this field a huge challenge. To address this problem, this study proposes a single-sample sub-network pruning method, which can identify redundant nodes by combining neuron coverage and the symbolic interval propagation method to reduce the network verification scale. In addition, to solve the problem of too many sub-networks to be pruned, according to the similarity of neuron coverage between samples, we propose a corresponding clustering algorithm to establish sub-networks for different categories of samples to improve the verification efficiency. We combine the MIPverify verification tool to validate the above method. Experiments show that the sub-networks can give the same robust validation results and similar robustness bounds as the original network, while greatly reducing the validation time and network size.

The real-time interaction between embedded software and its external environment is conducted through the interrupt mechanism. Since the interrupt request is random and responds according to priority, the execution of embedded software is non-sequential, which leads to the non-deterministic software behaviors. If these non-deterministic behaviors can be quantitatively pre-analyzed during the software design phase, the reliability of embedded software can be improved effectively. In this paper, we first provide an embedded software behavior model based on extended deterministic and stochastic Petri nets (EDSPN). Through EDSPN, the interrupt behavior of embedded software can be effectively modeled. Then we put forward a probabilistic model checking method of Continuous Stochastic Logic (CSL) for EDSPN to analyze embedded software behavior. For alleviating the state explosion problem, the above method uses the bounded model checking (BMC) technique. We present the model checking methods and the probability metric calculation methods for CSL operators under bounded semantics. Finally, by analyzing the EDSPN model of embedded software with multiple interrupts, we compare the analytical capabilities of BMC method and non-BMC method. The experiment shows that when the state space of EDSPN is large and is hard to calculate, the bounded checking algorithm can be used to approximate the software behavior. The conclusions obtained are helpful to understand the properties to be verified.

Discriminative pattern mining is one of the most important techniques in data mining. This challenging task is concerned with finding a set of patterns that occur with disproportionate frequency in data sets with various class labels. Such patterns are of great value for group difference detection and classifier construction. Research on finding interesting discriminative patterns in class-labeled data evolves rapidly and lots of algorithms have been proposed to specifically address this problem. Discriminative pattern mining techniques have proven their considerable value in biological data analysis. The archetypical applications in bioinformatics include phosphorylation motif discovery, differentially expressed gene identification, discriminative genotype pattern detection, etc. In this article, we present an overview of discriminative pattern mining and the corresponding effective methods, and subsequently we illustrate their applications to tackling the bioinformatics problems. In the end, we give a general discussion of potential challenges and future work for this task.