Program verification is a compelling way to ensure the dependable of software system, but the granularity of verification properties depends on the design of predicates. Definition of formal predicates is one of the prerequisites for automated software verification, the reason why predicate definitions of mutable data structures is relatively difficult, is that the trade-off between expressiveness of predicates and Satisfiability Modulo Theories (SMT) solver's proving capability. In this paper, we propose a method for constructing inductive predicates, which makes predicates more expressive and meanwhile ensures the provability of inductive properties in programs which manipulate mutable data structures through iteration. Furthermore, based on formal description of predicates about mutable data structures, a construction algorithm of complex inductive predicates is provided, which solves the dilemma of complicated programming of inductive property annotations during the verification process, and improves the automation of program verification. Experimental results show that the method can support the verification prototype to describe more complex properties about mutable data structures and alleviate the burden of automated theorem proving.
By analyzing the needs of Anhui University Library,the paper not only introduces the reasonable things in the building the specific computer network system of the Library and points that the public library computer network system in the course of construction should be focused,but also makes the analysis and reflection of the inadequacies of the system.
As the scale of software systems continues to increase, predicting program defects in a quick and efficient manner has become a significant research area. Recent studies have introduced deep learning models that use neural networks to extract code features and build classifiers for defect prediction. However, most existing research focuses on extracting code features at a single granularity and single level, resulting in a lack of rich code features and low prediction accuracy. To address this issue, this paper proposes a defect prediction framework based on feature fusion and alias analysis for predicting the presence of non-inferable aliases and vulnerabilities in programs. The proposed approach parses the program into two different program representations, namely Abstract Syntax Tree (AST) and Program dependency Graph (PDG), and extracts code features for feature fusion using Long Short-Term Memory (LSTM) networks and Graph Convolutional Networks (GCN), respectively. To evaluate the effectiveness of the proposed approach, the Software Assurance Reference Dataset (SARD) from the National Institute of Standards and Technology (NIST) is chosen as the experimental dataset. The classifiers constructed using the proposed approach are used to predict the presence of non-inferable aliases and vulnerabilities in programs. The experimental results demonstrate the effectiveness of the proposed approach in predicting program defects.
Formal verification is an important method to improve the high-confidence of software. However, it cannot be widely used for applications in the industry yet, mainly because of the insufficient proof power of theorem provers. The work of this paper focuses on the verification of quantified assertions describing program properties, and the verification process is based on the verification prototype system. For non-linear arithmetic in the quantified assertions verification, the Splitting-and-Merging method is proposed to transform the quantified assertions about the program, preserving original information and generating new quantified assertions, so that can be proved by automatic theorem prover. A Grouping method is proposed for the pointer programs with multiple quantified assertions of mutable data structures, it helps automatic theorem discover the association and properties between assertions of mutable data structures. Experimental results show that the verification prototype system can effectively solve the non-linear arithmetic problem and mutable data structures problem of the quantified assertions verification in program verification.
'/%3e%3cuse xlink:href='%23a' transform='rotate(23.036 .093 25.536)'/%3e%3cuse xlink:href='%23a' transform='rotate(45.87 1.273 16.18)'/%3e%3cuse xlink:href='%23a' transform='rotate(69.945 .996 12.078)'/%3e%3cuse xlink:href='%23a' transform='rotate(20.66 -19.689 31.932)'/%3e%3c/svg%3e)
'/%3e%3cuse xlink:href='%23a' transform='rotate(144 450 300)'/%3e%3cuse xlink:href='%23a' transform='rotate(216 450 300)'/%3e%3cuse xlink:href='%23a' transform='rotate(288 450 300)'/%3e%3c/svg%3e)