Termination of binary CLP programs has recently become an important question in the termination analysis community. the reason for this is due to the fact that some of the recent approaches to termination of logic pro...
详细信息
ISBN:
(纸本)3540266550
Termination of binary CLP programs has recently become an important question in the termination analysis community. the reason for this is due to the fact that some of the recent approaches to termination of logicprograms abstract the input program to a binary CLP program and conclude termination of the input program from termination of the abstracted program. In this paper we introduce a class of binary CLP programs such that their termination can be proved by using linear level mappings. We show that membership to this class is decidable and present a decision procedure. Further, we extend this class to programs such that their termination proofs require a combination of linear functions. In particular we consider as level mappings tuples of linear functions and piecewise linear functions.
Reachability logic has been applied to K rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-ge...
详细信息
ISBN:
(纸本)9783319944609;9783319944593
Reachability logic has been applied to K rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Constructor-based semantic unification, matching, and satisfiability procedures greatly increase the range of decidable background theories that can be used in reachability logic proofs. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.
logicprogramming is based on defining relations. Functions are often considered as syntactic sugar which can be transformed into predicates so that their logic is not used for computational purposes. In this paper, w...
详细信息
ISBN:
(纸本)9783031712937;9783031712944
logicprogramming is based on defining relations. Functions are often considered as syntactic sugar which can be transformed into predicates so that their logic is not used for computational purposes. In this paper, we present a method to use functions to improve the operational behavior of logicprograms without loosing the flexibility of logicprogramming. For this purpose, predicates and goals are transformed into functions and nested expressions. By evaluating these functions in a demand-driven manner wherever possible and taking potential failures into account, we ensure that the execution of the transformed programs will never require more steps than the original programs but can decrease the number of steps-in the best case reducing infinite search spaces to finite ones. thus, we obtain a systematic method to improve the operational behavior of logicprograms without changing their semantics.
In this work, we introduce a profiling scheme for modern functional logic languages covering notions like laziness, sharing, and non-determinism. Firstly, we instrument a natural (big-step) semantics in order to assoc...
详细信息
ISBN:
(纸本)3540266550
In this work, we introduce a profiling scheme for modern functional logic languages covering notions like laziness, sharing, and non-determinism. Firstly, we instrument a natural (big-step) semantics in order to associate a symbolic cost to each basic operation (e.g., variable updates, function unfoldings, case evaluations). While this cost semantics provides a formal basis to analyze the cost of a computation, the implementation of a cost-augmented interpreter based on it would introduce a huge overhead. therefore, we also introduce a sound transformationthat instruments a program such that its execution-under the standard semantics-yields not only the corresponding results but also the associated costs. Finally, we describe a prototype implementation of a profiler based on the developments in this paper.
the proceedings contain 10 papers. the special focus in this conference is on Practical Aspects of Declarative Languages. the topics include: Ontology-driven data semantics discovery for cyber-security;state space pla...
ISBN:
(纸本)9783319196855
the proceedings contain 10 papers. the special focus in this conference is on Practical Aspects of Declarative Languages. the topics include: Ontology-driven data semantics discovery for cyber-security;state space planning using transaction logic;on compiling linear logicprograms with comprehensions, aggregates and rule priorities;declaratively solving Google code jam problems with Picat;reactive single-page applications with dynamic dataflow;interpretation and compilation of constraint handling rules in curry;implementation and performance of probabilistic inference pipelines;a Haskell implementation of a rule-basedprogramtransformation for c programs;on logicprogramming representations of lambda terms and programming microcontrollers in OCAML.
In recent years techniques and systems have been developed to prove non-termination of logicprograms for certain classes of queries. In previous work, we developed such a system based on mode-information and a form o...
详细信息
ISBN:
(纸本)9783642205507
In recent years techniques and systems have been developed to prove non-termination of logicprograms for certain classes of queries. In previous work, we developed such a system based on mode-information and a form of loop checking performed at compile time. In the current paper we improve this technique by integrating type information in the analysis and by applying non-failure analysis and program specialization. It turns out that there are several classes of programs for which existing non-termination analyzers fail and for which our extended technique succeeds in proving non-termination.
We extend the range of security policies that can be guaranteed with proof carrying code from the classical type safety, control safety, memory safety, and space/time guarantees to more general security policies, such...
详细信息
ISBN:
(纸本)9783540714095
We extend the range of security policies that can be guaranteed with proof carrying code from the classical type safety, control safety, memory safety, and space/time guarantees to more general security policies, such as general resource and access control. We do so by means of (1) a specification logic for security policies, which is the past-time fragment of LTL, and (2) a synthesis algorithm generating reference monitor code and accompanying proof objects from formulae of the specification logic. To evaluate the feasibility of our approach, we developed a prototype implementation producing proofs in Isabelle/HOL.
We introduce negation to a symbolic-statistical modeling language PRISM and propose to eliminate negation by programtransformation called negation technique which is applicable to probabilistic logicprograms. We als...
详细信息
ISBN:
(纸本)3540266550
We introduce negation to a symbolic-statistical modeling language PRISM and propose to eliminate negation by programtransformation called negation technique which is applicable to probabilistic logicprograms. We also introduce finite PCFGs (probabilistic context free grammars) as PCFGs with finite constraints as part of generative modeling of stochastic HPSGs (head-driven phrase structure grammars). they are a subclass of log-linear models and allow exact computation of normalizing constants. We apply the negation technique to a PDCG (probabilistic definite clause grammar) program written in PRISM that describes a finite PCFG with a height constraint. the resulting program computes a normalizing constant for the finite PCFG in time linear in the given height. We also report on an experiment of parameter learning for a real grammar (ATR grammar) withthe height constraint. We have discovered that the height constraint does not necessarily lead to a significant decrease in parsing accuracy.
While there are well-understood methods for detecting loops whose iterations are independent and parallelizing them, there are comparatively fewer proposals that support parallel execution of a sequence of loops or ne...
详细信息
ISBN:
(纸本)9783642125911
While there are well-understood methods for detecting loops whose iterations are independent and parallelizing them, there are comparatively fewer proposals that support parallel execution of a sequence of loops or nested loops in the case where such loops have dependencies among them. this paper introduces a refined notion of independence, called eventual independence, that in its simplest form considers two loops, say loop, and loop, and captures the idea that for every i there exists k such that the i + 1-th iteration of loop, is independent from the j-th iteration of loop(1), for all j >= k. Eventual independence provides the foundation of a semantics-preserving programtransformation, called synchronized pipelining, that makes execution of consecutive or nested loops parallel, relying on a minimal number of synchronization events to ensure semantics preservation. the practical benefits of synchronized pipelining are demonstrated through experimental results on common algorithms such as sorting and Fourier transforms.
暂无评论