the proceedings contain 13 papers. the topics discussed include: proving termination with (Boolean) satisfaction;termination analysis of logicprograms based on dependency graphs;type-based homeomorphic embedding and ...
ISBN:
(纸本)3540787682
the proceedings contain 13 papers. the topics discussed include: proving termination with (Boolean) satisfaction;termination analysis of logicprograms based on dependency graphs;type-based homeomorphic embedding and its applications to online partial evaluation;towards a normal form for mercury programs;aggregates for CHR through programtransformation;preserving sharing in the partial evaluation of lazy functional programs;denotation by transformation: towards obtaining a denotational semantics by transformation to point-free style;generation of rule-based constraint solvers: combined approach;a scalable inclusion constraint solver using unification;a flexible, (C)LP-based approach to the analysis of object-oriented programs;snapshot generation in a constructive object-oriented modeling language;synthesis of data views for communicating processes;and action refinement in process algebra and security issues.
the proceedings contain 14 papers. the topics discussed include: how to talk to a human: the semantic web and the clash of the titans;constructing consensus logicprograms;supervising offline partial evaluation of log...
详细信息
ISBN:
(纸本)354071409X
the proceedings contain 14 papers. the topics discussed include: how to talk to a human: the semantic web and the clash of the titans;constructing consensus logicprograms;supervising offline partial evaluation of logicprograms using online techniques;improving offline narrowing-driven partial evaluation using size-change graphs;towards description and optimization of abstract machines in an extension of prolog;combining different proof techniques for verifying information flow security;on the automated synthesis of proof-carrying temporal reference monitors;synthesis of asynchronous systems;a comparative study of algorithmic debugging strategies;automated termination analysis for logicprograms by term rewriting;and detecting non-termination of term rewriting systems using an unfolding operator.
We present a new declarative compilation of logicprograms with constraints into variable-free relational theories which are then executed by rewriting. this translation provides an algebraic formulation of the abstra...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
We present a new declarative compilation of logicprograms with constraints into variable-free relational theories which are then executed by rewriting. this translation provides an algebraic formulation of the abstract syntax of logicprograms. Management of logic variables, unification, and renaming apart is completely elided in favor of algebraic manipulation of variable-free relation expressions. We prove the translation is sound, and the rewriting system complete with respect to traditional SLD semantics.
Concolic execution, a combination of concrete and symbolic execution, has become increasingly popular in recent approaches to model checking and test case generation. In general, an interpreter of the language is augm...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
Concolic execution, a combination of concrete and symbolic execution, has become increasingly popular in recent approaches to model checking and test case generation. In general, an interpreter of the language is augmented in order to also deal with symbolic values. In this paper, in contrast, we present an alternative approach that is based on a program instrumentation. Basically, the execution of the instrumented program in a standard environment produces a sequence of events that can be used to reconstruct the associated symbolic execution.
Proofs-as-programs is an approach to programsynthesis involving the transformation of constructive proofs of specification requirements into functional programs. Various authors have adapted the proofs-as-programs to...
详细信息
ISBN:
(纸本)9783540787686
Proofs-as-programs is an approach to programsynthesis involving the transformation of constructive proofs of specification requirements into functional programs. Various authors have adapted the proofs-as-programs to other logics and programming paradigms. this paper presents an adaptation of proofs-as-programs for the synthesis of distributed program protocols with side-effect-free data views, from proofs in a constructive proof-system for Hennessy-Milner logic.
Intuitionistic logicprogramming provides the notion of embedded implication in rule bodies, which can be used to reason about a current database modified by the antecedent. this can be applied to a system that transl...
详细信息
ISBN:
(纸本)9783319631394;9783319631387
Intuitionistic logicprogramming provides the notion of embedded implication in rule bodies, which can be used to reason about a current database modified by the antecedent. this can be applied to a system that translates SQL to Datalog to solve SQL WIth queries, for which relations are locally defined and can therefore be understood as locally added to the current database. In addition, assumptions in SQL queries as either adding or removing data can be modelled in this way as well, which is an interesting feature for decision-support scenarios. this work suggests a way to apply intuitionistic logicprogramming to SQL, and provides a pointer to a working system implementing this idea.
this book constitutes the thoroughly refereed post-conference proceedings of the 18thinternationalsymposium on logic-basedprogramsynthesis and transformation, lopstr 2008, held in Valencia, Spain, during July 17-1...
详细信息
ISBN:
(数字)9783642005152
ISBN:
(纸本)9783642005145
this book constitutes the thoroughly refereed post-conference proceedings of the 18thinternationalsymposium on logic-basedprogramsynthesis and transformation, lopstr 2008, held in Valencia, Spain, during July 17-18, 2008. the 11 revised full papers presented together with one invited talk were carefully reviewed and selected for inclusion in the book. lopstr traditionally solicits papers in the areas of specification, synthesis, verification, transformation, analysis, optimization, composition, security, reuse, applications and tools, component-based software development, software architectures, agent-based software development, and program refinement.
We propose an extension of Constraint Handling Rules (CHR) with aggregates such as sum, count, findall, and min. this new feature significantly improves the conciseness and expressiveness of the language. In this pape...
详细信息
ISBN:
(纸本)9783540787686
We propose an extension of Constraint Handling Rules (CHR) with aggregates such as sum, count, findall, and min. this new feature significantly improves the conciseness and expressiveness of the language. In this paper, we describe an implementation based on source-to-source transformations to CHR (extended with some low-level compiler directives). We allow user-defined aggregates and nested aggregate expressions over arbitrary guarded conjunctions of constraints. Both an on-demand and an incremental aggregate computation strategy are supported.
this paper introduces a modular framework for termination analysis of logicprogramming. To this end, we adapt the notions of dependency pairs and dependency graphs (which were developed for term rewriting) to the log...
详细信息
ISBN:
(纸本)9783540787686
this paper introduces a modular framework for termination analysis of logicprogramming. To this end, we adapt the notions of dependency pairs and dependency graphs (which were developed for term rewriting) to the logicprogramming domain. the main idea of the approach is that termination conditions for a program are established based on the decomposition of its dependency graph into its strongly connected components. these conditions can then be analysed separately by possibly different well-founded orders. We propose a constraint-based approach for automating the framework. then, for example, termination techniques based on polynomial interpretations can be plugged in as a component to generate well-founded orders.
暂无评论