Proving termination automatically for programs with explicit pointer arithmetic is still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Proving termination automatically for programs with explicit pointer arithmetic is still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that represents all possible runs of the program and that can be used to prove memory safety. this graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.
the proceedings contain 15 papers. the topics discussed include: partial type signatures for Haskell;abstract modular inference systems and solvers;sunroof: a monadic DSL for generating JavaScript;compiling DNA strand...
ISBN:
(纸本)9783319041315
the proceedings contain 15 papers. the topics discussed include: partial type signatures for Haskell;abstract modular inference systems and solvers;sunroof: a monadic DSL for generating JavaScript;compiling DNA strand displacement reactions using a functional programming language;two applications of the ASP-prolog system: decomposable programs and multi-context systems;towards modeling morality computationally withlogicprogramming;a declarative specification of giant number arithmetic;embedding foreign code;on the correctness and efficiency of lock-free expandable tries for tabled logic programs;typelets - a rule-based evaluation model for dynamic, statically typed user interfaces;expand: towards an extensible pandoc system;and generic generic programming.
We study finite model reasoning in expressive Horn description logics (DLs), starting with a reduction of finite ABox consistency to unrestricted ABox consistency. the reduction relies on reversing certain cycles in t...
详细信息
We study finite model reasoning in expressive Horn description logics (DLs), starting with a reduction of finite ABox consistency to unrestricted ABox consistency. the reduction relies on reversing certain cycles in the TBox, an approach that originated in database theory, was later adapted to the inexpressive DL DL-Lite(F), and is shown here to extend to the expressive Horn DL Horn-ALCFI. the model construction used to establish correctness makes the structure of finite models more explicit than existing approaches to finite model reasoning in expressive DLs that rely on solving systems of inequations over the integers. Since the reduction incurs an exponential blow-up, we then develop a dedicated consequence-based algorithm for finite ABox consistency in Horn-ALCFI that implements the reduction on-the-fly rather than executing it up-front. the algorithm has optimal worst-case complexity and provides a promising foundation for implementations. We next show that our approach can be adapted to finite (positive existential) query answering relative to Horn-ALCFI TBoxes, proving that this problem is EXPTIME-complete in combined complexity and PTimE-complete in data complexity. For finite satisfiability and subsumption, we also show that our techniques extend to Horn-SHIQ.
Among the most frequent reasoning tasks in the situation calculus are projection queries that query the truth of conditions in a future state of affairs. However, in long running action sequences solving the projectio...
详细信息
Among the most frequent reasoning tasks in the situation calculus are projection queries that query the truth of conditions in a future state of affairs. However, in long running action sequences solving the projection problem is complex. the main contribution of this work is a new technique which allows the length of the action sequences to be reduced by reordering independent actions and removing dominated actions;maintaining semantic equivalence with respect to the original action theory. this transformation allows for the removal of actions that are problematic with respect to progression, allowing for periodical update of the action theory to reflect the current state of affairs. We provide the logical framework for the general case and give specific methods for two important classes of action theories. the work provides the basis for handling more expressive cases, such as the reordering of sensing actions in order to delay progression, and forms an important step towards facilitating ongoing planning and reasoning by long-running agents. It provides a mechanism for minimising the need for keeping the action history while appealing to both regression and progression.
We study model-based diagnosis and propose a new approach of hybrid diagnosis combining black-box and white-box reasoning. We implemented and compared different diagnosis approaches including the standard hitting set ...
详细信息
the proceedings contain 20 papers. the special focus in this conference is on Web reasoning and Rule Systems. the topics include: Web reasoning for cultural heritage;planning with transaction logic;a generalization of...
ISBN:
(纸本)9783319111124
the proceedings contain 20 papers. the special focus in this conference is on Web reasoning and Rule Systems. the topics include: Web reasoning for cultural heritage;planning with transaction logic;a generalization of approximation fixpoint theory and application;query answering over contextualized RDF/OWL knowledge with forall-existential bridge rules;computing datalog rewritings for disjunctive datalog programs and description logic ontologies;towards mapping analysis in ontology-based data access;conjunctive query answering in finitely-valued fuzzy description logics;exchange-repairs: managing inconsistency in data exchange;rules and ontology based data access;semantic search for earth observartion products using ontology services;airport context analytics;navigating among educational resources in the web of linked data;investigating information diffusion in a multi-social-network scenario via answer set programming;web stream reasoning using probabilistic answer set programming;efficient federated debugging of lightweight ontologies;revisiting the hardness of query answering in expressive description logics;an ontology for container terminal operations;ontology-based answer extraction method;collective, incremental ontology alignment through query translation;disjunctive constraints in RDF and their application to context schemas;combining fuzzy and probabilistic reasoning for crowd-sourced categorization and tagging;visual editor for answer set programming and combining logic and business rule systems.
We propose a framework for reasoning about dynamic Web data, based on probabilistic Answer Set programming (ASP). Our approach, which is prototypically implemented, allows for the annotation of first-order formulas as...
详细信息
ISBN:
(纸本)9783319111131;9783319111124
We propose a framework for reasoning about dynamic Web data, based on probabilistic Answer Set programming (ASP). Our approach, which is prototypically implemented, allows for the annotation of first-order formulas as well as ASP rules and facts with probabilities, and for learning of such weights from examples (parameter estimation). Knowledge as well as examples can be provided incrementally in the form of RDF data streams. Optionally, stream data can be configured to decay over time. With its hybrid combination of various contemporary AI techniques, our framework aims at prevalent challenges in relation to data streams and Linked Data, such as inconsistencies, noisy data, and probabilistic processing rules.
We tackle the problem of partial correctness of programs processing structures defined as graphs. We introduce a kernel imperative programming language endowed with atomic actions that participate in the transformatio...
详细信息
Rule-based programming has been gaining a lot of interest in the industry lately, through the growing use of rules to model the behavior of software systems. A demand for verifying and analyzing rule based systems has...
详细信息
Special purpose embedded languages facilitate generating high-performance code from purely functional high-level code;for example, we want to program highly parallel GPUs without the usual high barrier to entry and th...
详细信息
暂无评论