Though obstruction-free progress property is weaker than other non-blocking properties including lock-freedom and wait-freedom,it has advantages that have led to the use of obstruction-free implementations for softwar...Though obstruction-free progress property is weaker than other non-blocking properties including lock-freedom and wait-freedom,it has advantages that have led to the use of obstruction-free implementations for software transactional memory(STM)and in anonymous and fault-tolerant distributed computing.However,existing work can only verify obstruction-freedom of specific data structures(e.g.,STM and list-based algorithms).In this paper,to fill this gap,we propose a program logic that can formally verify obstruction-freedom of practical implementations,as well as verify linearizability,a safety property,at the same time.We also propose informal principles to extend a logic for verifying linearizability to verifying obstruction-freedom.With this approach,the existing proof for linearizability can be reused directly to construct the proof for both linearizability and obstruction-freedom.Finally,we have successfully applied our logic to verifying a practical obstruction-free double-ended queue implementation in the first classic paper that has proposed the definition of obstruction-freedom.展开更多
Code defects can lead to software vulnerability and even produce vulnerability risks.Existing research shows that the code detection technology with text analysis can judge whether object-oriented code files are defec...Code defects can lead to software vulnerability and even produce vulnerability risks.Existing research shows that the code detection technology with text analysis can judge whether object-oriented code files are defective to some extent.However,these detection techniques are mainly based on text features and have weak detection capabilities across programs.Compared with the uncertainty of the code and text caused by the developer’s personalization,the programming language has a stricter logical specification,which reflects the rules and requirements of the language itself and the developer’s potential way of thinking.This article replaces text analysis with programming logic modeling,breaks through the limitation of code text analysis solely relying on the probability of sentence/word occurrence in the code,and proposes an object-oriented language programming logic construction method based on method constraint relationships,selecting features through hypothesis testing ideas,and construct support vector machine classifier to detect class files with defects and reduce the impact of personalized programming on detection methods.In the experiment,some representative Android applications were selected to test and compare the proposed methods.In terms of the accuracy of code defect detection,through cross validation,the proposed method and the existing leading methods all reach an average of more than 90%.In the aspect of cross program detection,the method proposed in this paper is superior to the other two leading methods in accuracy,recall and F1 value.展开更多
LP (Logic Programming) has been successfully applied to knowledge discovery in many fields. The execution of the LP is based on the evaluation of the first order predicate. Usually the information involved in the pred...LP (Logic Programming) has been successfully applied to knowledge discovery in many fields. The execution of the LP is based on the evaluation of the first order predicate. Usually the information involved in the predicates are local and homogenous, thus the evaluation process is relatively simple. However, the evaluation process become much more complicated when applied to KDD on the Internet where the information involved in the predicates maybe heterogeneous and distributed over many different sits. Therefor, we try to attack the problem in a multi agent system's framework so that the logic program can be written in a site independent style and deal easily with heterogeneous represented information.展开更多
Inductive logic programming adopts the standard horn lope program as its logic framework for inductivelearning. Due to the fact, however, that the expressive power of horn logic is relatively limited and the mechansm ...Inductive logic programming adopts the standard horn lope program as its logic framework for inductivelearning. Due to the fact, however, that the expressive power of horn logic is relatively limited and the mechansm ofnegation is mostly that of negation as failure, it is difficult to make full use of negative information and consequentlynot suitable for inductive learning. This Paper adopts nounal lope program as me language of inductive logic programsand presents accordingly a kind of semantics called Limited Negation semantics. The issues of direct denotation andinference of negation in concept induction are solved. The paper shows that LN is directly generalized for the semantics of Well-Founded in die significance Of optional negation and has superior theoretical features, especially the capability Of expressing and processing negation by introducing the constant ’false’. ExperimentS also show that the inductive concepts in learning are accurately interpreted with LN.展开更多
A method is presented for incrementally computing success patterns of logic programs. The set of success patterns of a logic program with respect to an abstraction is formulated as the success set of an equational log...A method is presented for incrementally computing success patterns of logic programs. The set of success patterns of a logic program with respect to an abstraction is formulated as the success set of an equational logic program modulo an equality theory that is induced by the abstraction. The method is exemplified via depth and stump abstractions. Also presented are algorithms for computing most general unifiers modulo equality theories induced by depth and stump abstractions.展开更多
During the last years, we have developed the FLOPER platform for providing a practical support to the so-called Multi-Adjoint Logic Programming approach (MALP in brief), which represents an extremely flexible framewor...During the last years, we have developed the FLOPER platform for providing a practical support to the so-called Multi-Adjoint Logic Programming approach (MALP in brief), which represents an extremely flexible framework into the Fuzzy Logic Programming arena. Nowadays, FLOPER is useful for compiling (to standard Prolog code), executing and debugging (by drawing execution trees) MALP programs, and it is ready for being extended in the near future with powerful transformation and optimization techniques designed in our research group during the recent past. Our last update consists in the integration of a graphical interface for a comfortable interaction with the system which allows, among other capabilities, the use of projects for packing scripts and auxiliary definitions of fuzzy sets/connectives, together with fuzzy programs and their associated lattices modeling truth-degrees beyond the simpler crisp case ﹛true;false﹜.展开更多
基于回答集语义的逻辑程序(Answer Set Programming,ASP)是描述性问题求解的典范,广泛应用于规划、诊断、调度以及生物信息学等领域。为了增强ASP的表达能力,一些工作在ASP引入了数据库系统中的聚合函数约束,并提出了SPT,FLP等语义,抽...基于回答集语义的逻辑程序(Answer Set Programming,ASP)是描述性问题求解的典范,广泛应用于规划、诊断、调度以及生物信息学等领域。为了增强ASP的表达能力,一些工作在ASP引入了数据库系统中的聚合函数约束,并提出了SPT,FLP等语义,抽象约束剥离聚合函数约束的具体形式成为研究ASP语义等性质的重要工具,并得到了抽象约束逻辑程序的各种回答集语义之间的关系和复杂性问题等的相关结果。对此,进一步研究了仅含凸抽象约束原子抽象约束逻辑的性质,证明了仅含凸抽象约束原子的正规逻辑程序判定是否存在FLP回答集是Σp 2完全的,其审慎推理和大胆推理分别是Πp 2完全的和Σp 2完全的。这些复杂性结果进一步理清了各类逻辑程序间的表达能力关系,为设计有效的回答集求解器提供了新的思路,也为进一步探索ASP在解决用凸抽象约束表示的问题中的应用提供了理论基础。展开更多
基金the National Natural Science Foundation of China(Grant No.61632005)。
文摘Though obstruction-free progress property is weaker than other non-blocking properties including lock-freedom and wait-freedom,it has advantages that have led to the use of obstruction-free implementations for software transactional memory(STM)and in anonymous and fault-tolerant distributed computing.However,existing work can only verify obstruction-freedom of specific data structures(e.g.,STM and list-based algorithms).In this paper,to fill this gap,we propose a program logic that can formally verify obstruction-freedom of practical implementations,as well as verify linearizability,a safety property,at the same time.We also propose informal principles to extend a logic for verifying linearizability to verifying obstruction-freedom.With this approach,the existing proof for linearizability can be reused directly to construct the proof for both linearizability and obstruction-freedom.Finally,we have successfully applied our logic to verifying a practical obstruction-free double-ended queue implementation in the first classic paper that has proposed the definition of obstruction-freedom.
基金This work was supported by National Key RD Program of China under Grant 2017YFB0802901.
文摘Code defects can lead to software vulnerability and even produce vulnerability risks.Existing research shows that the code detection technology with text analysis can judge whether object-oriented code files are defective to some extent.However,these detection techniques are mainly based on text features and have weak detection capabilities across programs.Compared with the uncertainty of the code and text caused by the developer’s personalization,the programming language has a stricter logical specification,which reflects the rules and requirements of the language itself and the developer’s potential way of thinking.This article replaces text analysis with programming logic modeling,breaks through the limitation of code text analysis solely relying on the probability of sentence/word occurrence in the code,and proposes an object-oriented language programming logic construction method based on method constraint relationships,selecting features through hypothesis testing ideas,and construct support vector machine classifier to detect class files with defects and reduce the impact of personalized programming on detection methods.In the experiment,some representative Android applications were selected to test and compare the proposed methods.In terms of the accuracy of code defect detection,through cross validation,the proposed method and the existing leading methods all reach an average of more than 90%.In the aspect of cross program detection,the method proposed in this paper is superior to the other two leading methods in accuracy,recall and F1 value.
文摘LP (Logic Programming) has been successfully applied to knowledge discovery in many fields. The execution of the LP is based on the evaluation of the first order predicate. Usually the information involved in the predicates are local and homogenous, thus the evaluation process is relatively simple. However, the evaluation process become much more complicated when applied to KDD on the Internet where the information involved in the predicates maybe heterogeneous and distributed over many different sits. Therefor, we try to attack the problem in a multi agent system's framework so that the logic program can be written in a site independent style and deal easily with heterogeneous represented information.
文摘Inductive logic programming adopts the standard horn lope program as its logic framework for inductivelearning. Due to the fact, however, that the expressive power of horn logic is relatively limited and the mechansm ofnegation is mostly that of negation as failure, it is difficult to make full use of negative information and consequentlynot suitable for inductive learning. This Paper adopts nounal lope program as me language of inductive logic programsand presents accordingly a kind of semantics called Limited Negation semantics. The issues of direct denotation andinference of negation in concept induction are solved. The paper shows that LN is directly generalized for the semantics of Well-Founded in die significance Of optional negation and has superior theoretical features, especially the capability Of expressing and processing negation by introducing the constant ’false’. ExperimentS also show that the inductive concepts in learning are accurately interpreted with LN.
文摘A method is presented for incrementally computing success patterns of logic programs. The set of success patterns of a logic program with respect to an abstraction is formulated as the success set of an equational logic program modulo an equality theory that is induced by the abstraction. The method is exemplified via depth and stump abstractions. Also presented are algorithms for computing most general unifiers modulo equality theories induced by depth and stump abstractions.
文摘During the last years, we have developed the FLOPER platform for providing a practical support to the so-called Multi-Adjoint Logic Programming approach (MALP in brief), which represents an extremely flexible framework into the Fuzzy Logic Programming arena. Nowadays, FLOPER is useful for compiling (to standard Prolog code), executing and debugging (by drawing execution trees) MALP programs, and it is ready for being extended in the near future with powerful transformation and optimization techniques designed in our research group during the recent past. Our last update consists in the integration of a graphical interface for a comfortable interaction with the system which allows, among other capabilities, the use of projects for packing scripts and auxiliary definitions of fuzzy sets/connectives, together with fuzzy programs and their associated lattices modeling truth-degrees beyond the simpler crisp case ﹛true;false﹜.
