Distributed virtual environment (DVE) refers to the simultaneous access of multiple users to a virtual environment, which can bring users an immersive experience of collaboration and participation. Currently, the relevant research on DVE is biased toward applications, mainly focusing on the systems design and development. There is less research on the abstract modeling of DVE, and these research works manually verify the correctness and completeness from the mathematical points of view. Therefore, this paper proposes a task-based DVE multi-entity functional modeling and mechanized verification method. First, after adding a task mechanism to the description logic (DL), we put forward a functional task description logic (FTDL), which can formally describe entities and tasks, and also functionally model entity operations and task executions. Then, three types of task-based entity behavioral consistency are explored, and the three types of theorems are mechanically verified in the Isabelle/HOL theorem prover. Finally, we discuss the scope of application of the FTDL and demonstrate the effectiveness of the FTDL model and verification method through a DVE for a kitchen. The proposed FTDL modeling and verification formal method is concise and expressive, and it can formally ensure the reliability of multi-entities' behaviors.

Network clustering (graph clustering) plays a crucial role in discovering the inherent structures within networks. MapReduce-based structural clustering algorithm for networks (MRSCANs) designed based on MapReduce's parallel computing model, efficiently handles large-scale data. However, MRSCAN can only be tested through experiments, and its correctness cannot be guaranteed. To address this issue, this article has achieved the first implementation of functional MRSCAN modeling and subjected it to rigorous mechanized verification in Isabelle. First, based on Google's MapReduce model type definition and higher-order generic functions, a general MapReduce-based algorithm functional modeling framework is constructed across the fundamental global phases of Map, Shuffle, and Reduce. Moreover, diverse strategies are devised during the Shuffle phases according to user requirements, enhancing the applicability and generality of the MapReduce functional modeling framework. Second, formalizing the definition of MRSCAN, is delineated into four key steps: similarity calculation, core calculation, dimension expansion, and structural clustering. Furthermore, the MapReduce functional modeling framework is applied to these four steps to achieve the functional modeling of MRSCAN, which improves efficiency compared to other structural clustering algorithm for networks (SCANs) algorithms. Lastly, a verification framework for MapReduce-based algorithms is proposed at both the global and shuffle stages. Based on this framework, the correctness and reliability of MRSCAN are ensured. The model framework and verification framework of MapReduce-based algorithms proposed in this article can not only address functional modeling and verification of MRSCAN but also provide a reference for a series of other MapReduce-based functional program designs and proofs.

The matroids have a wide range of applications in discrete mathematics, combinatorial mathematics, computer science and other fields. However, most of the researches about matroids focus on the mathematical level, and there is a lack of exploration on functional modelling and formal verification. In this paper, we propose a general functional modeling framework for matroids, which consists of the basic elements of matroids, the verification functions of basic properties, and the verification functions of matroids. Finally, the functional modeling framework of this paper is used to verify whether the 0-1 knapsack problem and the fractional knapsack problem conform to the matroid structure, thus exemplifying the correctness of the matroid functional modeling and the matroid verification function, and reflecting the validity and extensibility of this framework.

Bisimulation is a behavioral equivalence approach for discrete event systems. In recent years, bisimulation has been increasingly applied to nondeterministic fuzzy transition system (NFTS). Current researchers mainly focus on mathematical definitions of fuzzy bisimulation and the development of algorithms, however, the properties of definitions and the correctness of the algorithms are manually proven. Therefore, we formally define NFTS using the basic datatype package in theorem prover Isabelle/HOL. Subsequently, we originally present functional definitions of two critical fuzzy bisimulations (based on relational closed sets and relational lifting), and then mechanically verified the equivalence of these two definitions by using Isabelle/HOL. Furthermore, a relational lifting algorithm is formalized and its correctness is mechanically verified in this article. Finally, we present two case studies to validate the practicality of our approach. Compared with the mathematical definition and manual verification, our study demonstrated that a mechanized method for formalizing and verifying fuzzy bisimulation is more trustworthy, and it could be applied to various fuzzy bisimulation algorithms.

To enhance the efficiency of time security verification and fairness verification of auction contracts,an ab-stract modeling and verification method for role-based auction contracts was proposed.Firstly,the source code of the contract was abstractly modeled based on account roles and converted into a timed automaton network model.Formal de-scriptions of time security were provided and verified using the UPPAAL tool.Secondly,the mechanisms in the source code of the contract were extracted to establish a smart contract mechanism model,which was also converted into a timed automaton network model.Formal descriptions of four types of fairness were provided and verified using UPPAAL.Finally,the feasibility and effectiveness of the proposed method were demonstrated through two classic cases.

As a recursive method for finding the optimal solution to a problem,dynamic programming mainly solves the original problem by first solving the subproblems and then combining their solutions.Due to a large number of dependencies and constraints among its subproblems,the validation procedure is laborious,and especially the correctness verification of imperative dynamic programming algorithms is a challenge.Based on the functional modeling and verification of dynamic programming algorithms Isabelle/HOL,this study avoids dealing with complex dependencies and constraints in proving correctness by verifying the equivalence of imperative dynamic programming algorithms and their programs.Meanwhile,a framework for the design of imperative dynamic programming algorithmic programs and their mechanized verification are proposed.First,according to the optimization method(memo method)and properties(optimal substructure property and subproblems overlapping property)of dynamic programming algorithms,the problem specification is described,the recursive relations are inductively derived,and the loop invariants are formally constructed.Then,the IMP(minimalistic imperative programming language)code is generated based on the recursive relations.Second,the problem specification,loop invariants,and generated IMP code are fed into VCG(verification condition generator)to generate the verification condition for correctness automatically.Additionally,the verification condition is then mechanically verified in the Isabelle/HOL theorem prover.The algorithm is initially designed in the general form of an imperative dynamic programming algorithm and further instantiated to obtain specific algorithms.Finally,the effectiveness of the proposed framework is validated by case studies to provide references for automated derivation and verification of dynamic programming algorithms.

When cyber-physical systems (CPSs) are operational, its computing units frequently interact with complex and uncertain physical environments in time and space. To ensure the safety of the system, it is often necessary that the physical entities and information systems of CPS operate in a consistent manner at the temporal and spatial levels. However, most of the existing studies on spatio-temporal consistency modeling and verification of CPS are limited in the ability to deal with uncertainties. To address this issues, in this article, we propose a modeling and verification method for spatio-temporal consistency of CPS in uncertain environments. First, we propose a modeling language (stochastic spatio-temporal modeling language, SSTL) for the spatio-temporal domain of CPS. It can explicitly model the spatio-temporal constraints of CPS as well as deal with the spatio-temporal behavior of accompanying probabilities. Second, we propose a framework for spatio-temporal consistency verification. In the first step of this framework, we propose a worst-case time satisfiability algorithm to verifying the time safety of CPS. In the second step, we develop a prototype tool called “SSTL2NSHA” that is able to convert SSTL into the NHSA model supported by UPPAAL-statistical model checking (UPPAAL-SMC). Thereby the CPS model described by SSTL can be verified in UPPAAL-SMC for spatial safety constraints. Finally, we illustrate the effectiveness of the approach in this article with a traffic alert and collision avoidance system.

Software programming requires both API reference (know-what) knowledge and programming task (know-how) knowledge. Lots of programming know-what and know-how knowledge is documented in text, for example, API reference documentation and programming tutorials. To improve knowledge accessibility and usage, several recent studies use Natural Language Processing (NLP) methods to construct API know-what knowledge graph (API-KG) and programming task know-how knowledge graph (Task-KG) from software documentation. Although being promising, current API-KG and Task-KG are independent of each other, and thus are void of inherent connections between the two types of knowledge. Our empirical study on Stack Overflow questions confirms that only 36% of the API usage problems can be answered by the know-how or the know-what knowledge alone, while the rest questions requires a fusion of both. Inspired by this observation, we make the first attempt to fuse API-KG and Task-KG by API entity linking. This fusion creates nine categories of API semantic relations and two types of task semantic relations which are not present in the stand-alone API-KG or Task-KG. According to the definitions of these new API and task semantic relations, our approach dives deeper than surface-level API linking of API-KG and Task-KG, and infer nine categories of API semantic relations from task descriptions and two types of task semantic relations with the assistance of API-KG, which enrich the declaration or syntactic relations in the current API-KG and Task-KG. Our fused and semantically-enriched API-Task KG supports coherent API/Task-centric knowledge search by text or code queries. We have implemented our approach on Java programming documentation and built a web tool to search and explore API and programming task knowledge. Our evaluation confirms the high-accuracy of our knowledge extraction, fusion and enrichment methods, and the effectiveness and usefulness of our API-Task KG for answering Stack Overflow questions.

并行计算作为人工智能发展的动力,使得并行算法的可解释性和安全性成为人工智能领域重要研究方向.形式化方法以数理逻辑为基础,已经成为复杂安全苛求系统可信构建的重要方法,而函数式编程则在算法领域中具有更强的数学表达性.本文旨在提出一种基于模型驱动的分治并行函数式程序生成及自动验证方法,融合形式化方法,以解决目前分治并行程序生成和验证中缺乏可解释性、易错、低可信度等问题.首先,采用分划递推法和循环不变式等新策略推导出串行算法;然后,利用辅助函数和算法连接函数将其提升为并行算法,并使用我们提出的并行算法设计语言Radl+进行描述;进而,采用同态定理验证框架在 Isabelle 中验证算法连接函数满足同态定理,即提升后的算法可并行化;最后,提出了 Radl+→Haskell 转换规则,设计了"Radl+→Haskell 并行程序生成系统"软件原型.实验结果表明,本文能够生成和验证一系列算法的并行函数式程序,并且能够产生良好的加速比.本文方法不仅具有一定的可解释性,而且自动验证减少了传统手工验证易错性和繁琐的工作量,保证算法正确性和提高安全性,对大幅度提升高可信并行函数式程序的开发效率具有重要意义.

Programmers who work with smart contract development often encounter challenges in reusing code from repositories. This is due to the presence of two unknowns that can lead to non-functional and functional failures. These unknowns are implicit collaborations between functions and subtle differences among similar functions. Current code mining methods can extract syntax and semantic knowledge (known knowledge), but they cannot uncover these unknowns due to a significant gap between the known and the unknown. To address this issue, we formulate knowledge acquisition as a knowledge deduction task and propose an analytic flow that uses the function clone as a bridge to gradually deduce the known knowledge into the problem-solving knowledge that can reveal the unknowns. This flow comprises five methods: clone detection, co-occurrence probability calculation, function usage frequency accumulation, description propagation, and control flow graph annotation. This provides a systematic and coherent approach to knowledge deduction. We then structure all of the knowledge into a semantic-enriched code Knowledge Graph (KG) and integrate this KG into two software engineering tasks: code recommendation and crowd-scaled coding practice checking. As a proof of concept, we apply our approach to 5,140 smart contract files available on Etherscan.io and confirm high accuracy of our KG construction steps. In our experiments, our code KG effectively improved code recommendation accuracy by 6% to 45%, increased diversity by 61% to 102%, and enhanced NDCG by 1% to 21%. Furthermore, compared to traditional analysis tools and the debugging-with-the-crowd method, our KG improved time efficiency by 30 to 380 seconds, vulnerability determination accuracy by 20% to 33%, and vulnerability fixing accuracy by 24% to 40% for novice developers who identified and fixed vulnerable smart contract functions.

The traditional program refinement strategy cannot be refined to an executable program,and there are issues such as low verifi-cation reliability and automation.To solve the above problems,this paper proposesa nonlinear program construction and verification method based on partition recursion and Morgan's refinement rules.First,we use recursive definition technique to characterize the initial specification.The specification is then transformed into GCL(Guarded Command Language)programs using loop invariant derivation and Morgan's refinement rules.Furthermore,VCG(Verification Condition Generator)is used in the GCL program to generate the verification condition automatically.The Isabelle theorem prover then validates the GCL program's correctness.Finally,the GCL code generates a C++executable program automatically via the conversion system.The effectiveness of this method is demonstrated using binary tree preorder traversal program construction and verification as an example.This method addresses the problem that the construction process's loop in-variant is difficult to obtain and the refinement process is insufficiently detailed.At the same time,the method improves verification pro-cess automation and reduces the manual verification workload.

The program construction process is based on rigorous mathematical reasoning,which leads to a fully correct algorithmic pro-gram via step-by-step refinement of the program specifications.The existing program construction methods'refinement process is partly based on individual subjective speculation and analysis,which lacks a precise guidance method.Meanwhile,efficiency factors have usu-ally been ignored in the construction process,and most of the constructed abstract programs cannot be run directly by machines.In order to solve these problems,a novel program construction method for the sequence statistical class algorithms based on bidirectional scan induc-tion is proposed in this paper.The method takes into account the efficiency factor and thus improves the Morgan's refinement calculus.Fur-thermore,this paper validates the method's feasibility using an efficiency-sensitive sequential statistics class algorithm as a program con-struction example.The method proposed in this paper realizes the correctness construction process from program specifications to efficient executable programs.

API documentation, technical blogs and programming Q&A sites contain numerous partial code that can be reused in programming tasks, but often these code are uncompilable due to unresolved names and syntax errors. To facilitate partial code reuse, we propose the Partial Code Reuse Chain (PCR-Chain) for resolving fully-qualified names (FQNs) and fixing last-mile syntax errors in partial code based on a giant large language model (LLM) like ChatGPT. Methodologically, PCR-Chain is backed up by the underlying global-level prompt architecture (which combines three design ideas: hierarchical task breakdown, prompt composition, and a mix of prompt-based AI and non-AI units) and the local-level prompt design. Technically, we propose PCR-Chain, which employs in-context learning rather than symbolic, costly training methods. Experimental results demonstrate that in dynamically-typed languages (Python), PCR-Chain outperforms current state-of-the-art (SOTA) 5% accuracy like RING. For statically-type languages (Java), our approach achieves high accuracy of 80.5% in resolving both non-FQNs and last-mile syntax errors, surpassing SOTA methods (RING) that can only address last-mile syntax errors. The correct execution of the unit, module, and PCR-Chain demonstrates the effectiveness of the prompt design, composition, and architecture and opens up possibilities for building software engineering tools based on LLMs, replacing traditional program analysis methods.

API documentation, technical blogs and programming Q&A sites contain a large amount of partial code that can be reused in programming tasks. However, due to unresolved simple names and last-mile syntax errors, such partial code is frequently not compilable. To facilitate partial code reuse, we develop PCR-Chain for resolving FQNs and fixing last-mile syntax errors in partial code based on a giant pre-trained code model (e.g., Copilot). Methodologically, PCR-Chain is backed up by the underlying global-level prompt architecture (which combines three design ideas: hierarchical task breakdown, prompt composition including sequential and conditional structures, and a mix of prompt-based AI and non-AI units) and the local-level prompt design. Technically, we propose PCR-Chain, which employs in-context learning rather than supervised fine-tuning with gradient updates on downstream task data. This approach enables the frozen, giant pre-trained code model to learn the desired behavior for a specific task through behavior-describing prompts and imitate it to complete the task. Experimental results show that PCR-Chain automatically resolves the FQNs and fixes last-mile syntax errors in 50 partial code samples collected from Stack Overflow with high success rates, without requiring any program analysis. The correct execution of the unit, module, and PCR-Chain demonstrates the effectiveness of the prompt design, prompt composition, and prompt architecture. Website:https://github.com/SE-qinghuang/PCR-ChainDemoVideo: https://youtu.be/6HGRNc2JE

The smart contract, a self-executing program on the blockchain, is key to programmable finance. However, the rise of smart contract use has also led to an increase in vulnerabilities that attract illegal activity from hackers. Traditional manual approaches for vulnerability detection, relying on domain experts, have limitations such as low automation and weak generalization. In this paper, we propose a deep learning approach that leverages domain-specific features and an attention mechanism to accurately detect vulnerabilities in smart contracts. Our approach reduces the reliance on manual input and enhances generalization by continuously learning code patterns of vulnerabilities, specifically detecting various types of vulnerabilities such as reentrancy, integer overflow, forced Ether injection, unchecked return value, denial of service, access control, short address attack, tx.origin, call stack overflow, timestamp dependency, random number dependency, and transaction order dependency vulnerabilities. In order to extract semantic information, we present a semantic distillation approach for detecting smart contract vulnerabilities. This approach involves using a syntax parser, Slither, to segment the code into smaller slices and word embedding to create a matrix for model training and prediction. Our experiments indicate that the BILSTM model is the best deep learning model for smart contract vulnerability detection task. We looked at how domain features and self-attentiveness mechanisms affected the ability to identify 12 different kinds of smart contract vulnerabilities. Our results show that by including domain features, we significantly increased the F1 values for 8 different types of vulnerabilities, with improvements ranging from 7.35% to 48.58%. The methods suggested in this study demonstrate a significant improvement in F1 scores ranging from 4.18% to 38.70% when compared to conventional detection tools like Oyente, Mythril, Osiris, Slither, Smartcheck, and Securify. This study provides developers with a more effective method of detecting smart contract vulnerabilities, assisting in the prevention of potential financial losses. This research provides developers with a more effective means of detecting smart contract vulnerabilities, thereby helping to prevent potential financial losses.

Implementations that follow the functional programming paradigm are being used in more and more domains. As functional programming paradigm has mathematical reference transparency, refinement to functional programs contributes to improving the reliability of the transformation process and simplifying the refinement steps. However, it is a challenge to generate functional programs from specifications. Most existing transformation methods refine specifications into abstract algorithm-level programs based on loop invariants rather than functional programs. This paper proposes a novel functional program generation method based on the partition-recursion refinement rule. It establishes a novel program refinement framework based on functional theory for the first time. This is the first study to regard the whole program refinement process as a composition of abstract functions. This paper designs a recurrence-based algorithm design language (Radl+) and implements a software prototype to map Radl+ algorithms into executable Haskell programs. To prove the feasibility and efficiency of this method, this paper transforms the polynomial multiplication problem from a specification into an executable Haskell program. This case shows that compared with existing approaches, the proposed method can simplify the transformation steps and reduce the number of lines of generated code from 38 to 10.

API recommendation methods have evolved from literal and semantic keyword matching to query expansion and query clarification. The latest query clarification method is knowledge graph (KG)-based, but limitations include out-of-vocabulary (OOV) failures and rigid question templates. To address these limitations, we propose a novel knowledge-guided query clarification approach for API recommendation that leverages a large language model (LLM) guided by KG. We utilize the LLM as a neural knowledge base to overcome OOV failures, generating fluent and appropriate clarification questions and options. We also leverage the structured API knowledge and entity relationships stored in the KG to filter out noise, and transfer the optimal clarification path from KG to the LLM, increasing the efficiency of the clarification process. Our approach is designed as an AI chain that consists of five steps, each handled by a separate LLM call, to improve accuracy, efficiency, and fluency for query clarification in API recommendation. We verify the usefulness of each unit in our AI chain, which all received high scores close to a perfect 5. When compared to the baselines, our approach shows a significant improvement in MRR, with a maximum increase of 63.9% higher when the query statement is covered in KG and 37.2% when it is not. Ablation experiments reveal that the guidance of knowledge in the KG and the knowledge-guided pathfinding strategy are crucial for our approach's performance, resulting in a 19.0% and 22.2% increase in MAP, respectively. Our approach demonstrates a way to bridge the gap between KG and LLM, effectively compensating for the strengths and weaknesses of both.

传统的程序求精策略无法求精至可执行程序,且存在验证的可信度低和自动化程度不高的问题.针对上述问题,提出一种较完整的程序求精策略并给出自动验证方法.使用递归定义函数技术刻画问题规约,基于Morgan精化规则程序求精至IMP程序,并使用验证条件生成器(verification condition generator,VCG)自动生成验证条件,通过Isabelle定理证明器验证IMP程序的正确性,最后利用开发平台自动生成C++可执行程序.以最长标志基因序列问题为实例进行程序求精和自动验证,检验了所提策略的有效性.该策略提高了算法程序开发的正确性,减轻了传统验证烦琐的工作量.

In the formal derivation and proof of binary tree algorithms, Dijkstra's weakest predicate method is commonly used. However, the method has some drawbacks, including a time-consuming derivation process, complicated loop invariants, and the inability to generate executable programs from the specification. This paper proposes a unified strategy for the formal derivation and proof of binary tree non-recursive algorithms to address these issues. First, binary tree problem solving sequences are decomposed into two types of recursive relations based on queue and stack, and two corresponding loop invariant templates are constructed. Second, high-reliability Apla (abstract programming language) programs are derived using recursive relations and loop invariants. Finally, Apla programs are converted automatically into C++ executable programs. Two types of problems with binary tree queue and stack recursive relations are used as examples, and their formal derivation and proof are performed to validate the proposed strategy's effectiveness. This strategy improves the efficiency and correctness of binary tree algorithm derivation.

Web服务测试与验证是保证Web服务功能正确的关键,目前大多数Web服务的研究无法对程序路径穷举遍历,不能保证分析的完备性.针对该不足,在基于模型驱动的3阶段Web服务模型转换生成方法的基础上,该文对转换生成的Java代码进行符号执行与形式化验证.符号执行方法可对程序运行的所有路径进行分析,为程序测试提供高覆盖率的测试用例,可以触发深层的程序错误,进而在Java代码中加入JML方法契约,可对Web服务进行形式化验证.通过PayPal Web服务案例,采用模型驱动的方法将Web服务模型转换生成方法生成Java代码,使用自动化工具对Java代码进行符号执行;将Radl-WS服务建模语言转换为JML方法契约,并对Java代码进行形式化验证.符号执行与形式化验证方法确保了生成的Java代码可靠性与正确性,提高了自动化程度.