the proceedings contain 289 papers from the logicbasedprogramsynthesis and transformation: 14thinternationalsymposium, LOPSTER 2004. Revised Selected Papers. Topics discussed include searching semantically equiva...
详细信息
the proceedings contain 289 papers from the logicbasedprogramsynthesis and transformation: 14thinternationalsymposium, LOPSTER 2004. Revised Selected Papers. Topics discussed include searching semantically equivalent code fragments in logicprograms;determinacy analysis for logicprograms using mode and type information;mechanical verification of automatic synthesis of fault-tolerant programs;fully automatic binding-time analysis for prolog;logical mobility and locality types;negation elimination for finite PCFGs;specialization of concurrent guarded multi-set transformation rules;efficient local unfolding with ancestor stacks for full prolog;and natural rewriting for general term rewriting systems.
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.
the proceedings contain 14 papers. the topics discussed include: towards scalable partial evaluation of declarative programs;deciding full branching time logic by programtransformation;a transformational approach for...
ISBN:
(纸本)3642125913
the proceedings contain 14 papers. the topics discussed include: towards scalable partial evaluation of declarative programs;deciding full branching time logic by programtransformation;a transformational approach for proving properties of the CHR constraint store;the dependency triple framework for termination of logicprograms;goal-directed and relative dependency pairs for proving the termination of narrowing;LP with flexible grouping and aggregates using modes;on inductive and coinductive proofs via unfold/fold transformations;coinductive logicprogramming with negation;refining exceptions in four-valued logic;towards a framework for constraint-based test case generation;using rewrite strategies for testing BUpL agents;towards just-in-time partial evaluation of prolog;program parallelization using synchronized pipelining;and defining datalog in rewriting logic.
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.
We provide an approach to formally analyze the computational behavior of coroutines in logicprograms and to compile these computations into new programs, not requiring any support for coroutines. the problem was alre...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
We provide an approach to formally analyze the computational behavior of coroutines in logicprograms and to compile these computations into new programs, not requiring any support for coroutines. the problem was already studied near to 30 years ago, in an analysis and transformation technique called Compiling Control. However, this technique had a strong ad hoc flavor: the completeness of the analysis was not well understood and its symbolic evaluation was also very ad hoc. We show how Abstract Conjunctive Partial Deduction, introduced by Leuschel in 2004, provides an appropriate setting to redefine Compiling Control. Leuschel's framework is more general than the original formulation, it is provably correct, and it can easily be applied for simple examples. We also show that the Abstract Conjunctive Partial Deduction framework needs some further extension to be able to deal with more complex examples.
As part of a platform for computer-assisted verification, we present an intermediate representation of programs that is both language independent and appropriate for the generation of verification conditions. We show ...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
As part of a platform for computer-assisted verification, we present an intermediate representation of programs that is both language independent and appropriate for the generation of verification conditions. We show how many imperative and functional languages can be translated to this generic intermediate representation, and how the generated conditions reflect the axiomatic semantics of the original program. At this representation level, loop invariants and preconditions of recursive functions belonging to the original program are represented by assertions placed at certain edges of a directed graph. the paper defines the generic representation, sketches the transformation algorithms, and describes how the places where the invariants should be placed are computed. Assuming that, either manually or assisted by the platform, the invariants have been settled, it is shown how the verification conditions are generated. A running example illustrates the process.
We propose an automated technique for inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting ...
详细信息
ISBN:
(纸本)9783319631394;9783319631387
We propose an automated technique for inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KernelC in the K framework, we enrich the symbolic execution facilities recently provided by C with novel capabilities for assertion synthesisthat are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that explains the execution of a (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KindSpec 2.0, which generates logical axioms that define the precise input/ output behavior of the C routines.
We present a generic scheme for the abstract debugging of functional logicprograms. We associate to programs a semantics based on a (continuous) immediate consequence operator. P[R], which models correctly the powerf...
详细信息
ISBN:
(纸本)9783642205507
We present a generic scheme for the abstract debugging of functional logicprograms. We associate to programs a semantics based on a (continuous) immediate consequence operator. P[R], which models correctly the powerful features of modern functional logic languages (non-deterministic, non-strict functions defined by non-confluent programs and call-time choice behaviour). then, we develop an effective debugging methodology which is based on abstract interpretation: by approximating the intended specification of the semantics of R we derive a finitely terminating bottom-up diagnosis method, which can be used statically. Our debugging framework does not require the user to provide error symptoms in advance and is applicable with partial specifications and even partial programs.
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.
In this work, we devise an analysis that searches for semantically equivalent code fragments within a given logicprogram. the presence of duplicated code (or functionality) is a primary indication that the design of ...
详细信息
ISBN:
(纸本)3540266550
In this work, we devise an analysis that searches for semantically equivalent code fragments within a given logicprogram. the presence of duplicated code (or functionality) is a primary indication that the design of the program can be improved by performing a so-called refactoring transformation. Within the framework of our analysis, we formally characterize three situations of duplicated functionality and their associated refactorings: the extraction of a duplicated goal into a new predicate, the removal of equivalent predicates and the generalization of two predicates into a higher-order predicate. the resulting analysis detects in a completely automatic way what program fragments are suitable candidates for the considered refactoring transformations.
暂无评论