检索结果-内蒙古大学图书馆

13th IEEE international conference on Trust Security and Privacy in Computing and Communications (TrustCom)

作者： Han, Zhihui Cheng, Liang Zhang, Yang Zeng, Shuke Deng, Yi Sun, Xiaoshan Chinese Acad Sci Inst Software Trusted Comp & Informat Assurance Lab Beijing 100864 Peoples R China

ISBN: (纸本)9781479965137

Android is a modern and popular software platform for smartphones. To manage information and features on smartphones, Android employs intent-based mechanism for interapplication or intra-application communication and provides a permission-based security model that requires each application to explicitly request permissions in its manifest file. However, misconfiguration defined in manifest files and that embedded in application code may result in vulnerabilities due to developer confusion and general misuse of the features provided by Android. In this paper, we propose a logic-programming-based approach to analyze smartphones and discover misconfiguration vulnerabilities in Android manifest file and application code. To enable misconfiguration vulnerability analysis and detection, we develop a static technique to extract security related information from application code, and employ logic predicates to describe various vulnerabilities. Based on this approach, we developed a tool called SADroid to systematically analyze and detect misconfiguration vulnerabilities in Android smartphones. Our results with two representative phones show that the inherent weakness of Android permission model and developers' programming errors make Android vulnerable to some attacks.

关键词： Android smartphone static analysis misconfiguration vulnerability logic programming

来源：评论

学校读者我要写书评

暂无评论

Development of Methods and Algorithms Based on Object-Oriented logic programming for Video Monitoring of Laboratory Rodents 13

Development of Methods and Algorithms Based on Object-Orient...

引用

13th international conference on Signal-Image Technology and Internet-Based Systems (SITIS)

作者： Morozov, Alexei A. Sushkova, Olga S. Vaniya, Sandipkumar M. RAS Kotelnikov Inst Radio Engn & Elect Mokhovaya 11-7 Moscow 125009 Russia Cent Salt & Marine Chem Res Inst Gijubhai Badheka Marg Bhavnagar 364002 Gujarat India

ISBN: (纸本)9781538642832

the problem of video monitoring of laboratory rodents by the means of object-oriented logic programming is considered. the videos are produced in neurophysiological experiments on the study of convulsive electrical activity of the brain cortex. Videos of behaviour of laboratory rats were recorded simultaneously with electroencephalograms (EEG) in the animals. A comparison of EEG data with the behaviour of the animals is necessary because sharp motions of the animals can result in EEG signals that are very similar to the epileptic discharges. thus, the first task of the video monitoring is recognition of the sharp motions of the animals and using this information for proper interpretation of the results of the experiments. the second task of the video monitoring is analysis of behaviour of animals in cognitive testing. Essential feature of the video records is in that the experiments are conducted in the same cage where the animal lives, that is, the background of the cage is sawdust. the colour of the animals is about the same as the colour of the sawdust;thus the detection of the animals is not a simple task. In the paper, development of low-level algorithms for video analysis as well as logical methods for the analysis of the animal behaviour is discussed. the methods and algorithms are implemented in the Actor Prolog object-oriented logic language.

关键词： intelligent video surveillance intelligent video monitoring laboratory animals neurophysiological experiment rodent rat behaviour analysis Actor Prolog object-oriented logic programming Prolog to Java translation

来源：评论

学校读者我要写书评

暂无评论

13th international conference on Automated Deduction, Cade 1996

13th International Conference on Automated Deduction, Cade 1...

引用

13th international conference on Automated Deduction, CADE 1996

ISBN: (纸本)3540615113

the proceedings contain 63 papers. the special focus in this conference is on Automated Deduction. the topics include: A resolution theorem prover for intuitionistic logic;proof-terms for classical and intuitionistic resolution;proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification;extensions to a generalization critic for inductive proof;learning domain knowledge to improve theorem proving;patching faulty conjectures;internal analogy in theorem proving;termination of theorem proving by reuse;termination of algorithms over non-freely generated data types;a proof checker with abstraction;the design of the CADE-13 ATP system competition;elimination of predicate quantifiers;a geometry theorem prover;structuring metatheory on inductive definitions;an embedding of ruby in isabelle;mechanical verification of mutually recursive procedures;decentralized traffic control system based on logic programming;presenting machine-found proofs;towards an expert system for many-valued logics;a system presentation;an introduction to geometry expert;simple competitive parallel theorem provers;unification algorithms cannot be combined in polynomial time;unification and matching modulo nilpotence;an improved lower bound for the elementary theories of trees;prolog technology theorem prover for default reasoning;an updated system description;generating models by SEM;optimizing proof search in model elimination;an abstract machine for fixed-order dynamically stratified programs;unification in pseudo-linear sort theories is decidable;theorem proving with group presentations;transforming termination by self-labelling;theorem proving in cancellative abelian monoids and on the practical value of different definitional translations to normal form.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Temporal logic properties of Java objects

引用

JOURNAL OF SYSTEMS AND SOFTWARE 2003年第3期68卷 243-251页

作者： Iosif, R Sisto, R Politecn Torino Dipartimento Automat I-10129 Turin Italy

Applying finite-state verification techniques to software systems looks attractive because they are capable of detecting very subtle defects in the logic design of these systems. Nevertheless, the integration of existing formal verification tools within programming environments is not yet easy, mainly because of the semantic gap between widely used programming languages and the languages used to describe system requirements. In this paper, we propose a formal requirement specification notation based on linear temporal logic, with regard to object oriented program elements, such as classes and interfaces. the specification is inherently object oriented and is meant for the verification of concurrent and distributed software systems. (C) 2003 Elsevier Inc. All rights reserved.

关键词： source code verification linear temporal logic object orientation Java

来源：评论

学校读者我要写书评

暂无评论

On formal verification in imperative multivalued programming over continuous data types 13

On formal verification in imperative multivalued programming...

引用

13th international conference on Computability and Complexity in Analysis, CCA 2016

作者： Müller, Norbert Park, Sewon Preining, Norbert Ziegler, Martin Trier University Germany KAIST Korea Republic of JAIST Japan

来源：评论

学校读者我要写书评

暂无评论

Randomised restarted search in ILP

引用

MACHINE LEARNING 2006年第1-3期64卷 183-208页

作者： Zelezny, Filip Srinivasan, Ashwin Page, C. David, Jr. Czech Tech Univ CR-16635 Prague Czech Republic IBM India Res Lab New Delhi India Univ Wisconsin Madison WI USA

Recent statistical performance studies of search algorithms in difficult combinatorial problems have demonstrated the benefits of randomising and restarting the search procedure. Specifically, it has been found that if the search cost distribution of the non-restarted randomised search exhibits a slower-than-exponential decay (that is, a "heavy tail"), restarts can reduce the search cost expectation. We report on an empirical study of randomised restarted search in ILP. Our experiments conducted on a high-performance distributed computing platform provide an extensive statistical performance sample of five search algorithms operating on two principally different classes of ILP problems, one represented by an artificially generated graph problem and the other by three traditional classification benchmarks (mutagenicity, carcinogenicity, finite element mesh design). the sample allows us to (1) estimate the conditional expected value of the search cost (measured by the total number of clauses explored) given the minimum clause score required and a "cutoff" value (the number of clauses examined before the search is restarted), (2) estimate the conditional expected clause score given the cutoff value and the invested search cost, and (3) compare the performance of randomised restarted search strategies to a deterministic non-restarted search. Our findings indicate striking similarities across the five search algorithms and the four domains, in terms of the basic trends of both the statistics (1) and (2). Also, we observe that the cutoff value is critical for the performance of the search algorithm, and using its optimal value in a randomised restarted search may decrease the mean search cost (by several orders of magnitude) or increase the mean achieved score significantly with respect to that obtained with a deterministic non-restarted search.

关键词： inductive logic programming randomized search Monte Carlo study

来源：评论

学校读者我要写书评

暂无评论

On the acceptability of arguments and its fundamental role in nonmonotonic reasoning and logic programming

On the acceptability of arguments and its fundamental role i...

引用

Proceedings of the 13th international Joint conference on Artificial Intelligence

作者： Dung, Phan Minh

来源：评论

学校读者我要写书评

暂无评论

Quantitative pharmacophore models with inductive logic programming

Quantitative pharmacophore models with inductive logic progr...

引用

13th international conference on inductive logic programming

作者： Srinivasan, Ashwin Page, David Camacho, Rui King, Ross Indian Inst Technol IBM India Res Lab New Delhi India Univ Madison Dept Biostat Madison WI USA LIACC CIUP P-4150 Oporto Portugal Univ Wales Dept Comp Sci Aberystwyth Dyfed Wales

three-dimensional models, or pharmacophores, describing Euclidean constraints on the location on small molecules of functional groups (like hydrophobic groups, hydrogen acceptors and donors, etc.), are often used in drug design to describe the medicinal activity of potential drugs (or 'ligands'). this medicinal activity is produced by interaction of the functional groups on the ligand with a binding site on a target protein. In identifying structure-activity relations of this kind there are three principal issues: (1) It is often difficult to "align" the ligands in order to identify common structural properties that may be responsible for activity;(2) Ligands in solution can adopt different shapes (or 'conformations') arising from torsional rotations about bonds. the 3-D molecular substructure is typically sought on one or more low-energy conformers;and (3) Pharmacophore models must, ideally, predict medicinal activity on some quantitative scale. It has been shown that the logical representation adopted by inductive logic programming (ILP) naturally resolves many of the difficulties associated with the alignment and multi-conformation issues. However, the predictions of models constructed by ILP have hitherto only been nominal, predicting medicinal activity to be present or absent. In this paper, we investigate the construction of two kinds of quantitative pharmacophoric models with ILP: (a) Models that predict the probability that a ligand is "active";and (b) Models that predict the actual medicinal activity of a ligand. Quantitative predictions are obtained by the utilising the following statistical procedures as background knowledge: logistic regression and naive Bayes, for probability prediction;linear and kernel regression, for activity prediction. the multi-conformation issue and, more generally, the relational representation used by ILP results in some special difficulties in the use of any statistical procedure. We present the principal issues and some solut

关键词： pharmacophore models ILP statistical relational learning

来源：评论

学校读者我要写书评

暂无评论

Learning to parse database queries using inductive logic programming

Learning to parse database queries using inductive logic pro...

引用

Proceedings of the 1996 13th National conference on Artificial Intelligence. Part 2 (of 2)

作者： Zelle, John M. Mooney, Raymond J. Drake Univ Des Moines United States

this paper presents recent work using the CHILL parser acquisition system to automate the construction of a natural-language interface for database queries. CHILL treats parser acquisition as the learning of search-control rules within a logic program representing a shift-reduce parser and uses techniques from inductive logic programming to learn relational control knowledge. Starting with a general framework for constructing a suitable logical form, CHILL is able to train on a corpus comprising sentences paired with database queries and induce parsers that map subsequent sentences directly into executable queries. Experimental results with a complete database-query application for U.S. geography show that CHILL is able to learn parsers that outperform a preexisting, hand-crafted counterpart. these results demonstrate the ability of a corpus-based system to produce more than purely syntactic representations. they also provide direct evidence of the utility of an empirical approach at the level of a complete natural language application.

关键词： Natural language processing systems

来源：评论

学校读者我要写书评

暂无评论

13th international Workshop on Computer Science logic, CSL 1999 and 8th Annual conference of the European Association for Computer Science logic, EACSL 1999

引用

13th international Workshop on Computer Science logic, CSL 1999 and held as international Workshops on Computer Science logic, EACSL 1999

ISBN: (纸本)3540665366

the proceedings contain 41 papers. the special focus in this conference is on Verification, Temporal logic, Lambda Calculus, Linear logic and Descriptive Complexity. the topics include: Topological queries in spatial databases;constraint-based analysis of broadcast protocols;applicative control and computational complexity;applying rewriting techniques to the verification of erlang processes;an expressively complete temporal logic without past tense operators for mazurkiewicz traces;using fields and explicit substitutions to implement objects and functions in a de bruijn setting;a linear logical view of linear type isomorphisms;choice logic programs and Nash equilibria in strategic games;resolution method for modal logic with well-founded frames;fixpoint alternation and the game quantifier;open least element principle and bounded query computation;anti-symmetry of higher-order subtyping;monadic presentations of lambda terms using generalized inductive types;a logical viewpoint on process-algebraic quotients;data-refinement for call-by value programming languages and interactive theorem proving using type theory.

关键词：

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：