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 a general framework for assertion-based debugging of constraint logicprograms. Assertions are linguistic constructions for expressing properties of programs. We define several assertion schemas for writing...
详细信息
ISBN:
(纸本)3540676287
We propose a general framework for assertion-based debugging of constraint logicprograms. Assertions are linguistic constructions for expressing properties of programs. We define several assertion schemas for writing (partial) specifications for constraint logicprograms using quite general properties, including user-defined programs. the framework is aimed at detecting deviations of the program behavior (symptoms) with respect to the given assertions, either at compile-time (i.e., statically) or run-time (i.e., dynamically). We provide techniques for using information from global analysis both to detect at compile-time assertions which do not hold in at least one of the possible executions (i.e., static symptoms) and assertions which hold for all possible executions (i.e., statically proved assertions). We also provide programtransformations which introduce tests in the program for checking at run-time those assertions whose status cannot be determined at compile-time. Boththe static and the dynamic checking are provably safe in the sense that all errors flagged are definite violations of the specifications. Finally, we report briefly on the currently implemented instances of the generic framework.
this article proposes a method for proving the correctness of graph algorithms by manipulating their spanning trees enriched with additional references. We illustrate this concept with a proof of the correctness of a ...
详细信息
ISBN:
(纸本)9783642205507
this article proposes a method for proving the correctness of graph algorithms by manipulating their spanning trees enriched with additional references. We illustrate this concept with a proof of the correctness of a (pseudo-)imperative version of the Schorr-Waite algorithm by refinement of a functional one working on trees. It is composed of two orthogonal steps of refinement - functional to imperative and tree to graph - finally merged to obtain the result. Our imperative specifications use monadic constructs and syntax sugar, making them close to common imperative languages. this work has been realized within the Isabelle/HOL proof assistant.
this book constitutes the thoroughly refereed post-proceedings of the 20thinternationalsymposium on logic-basedprogramsynthesis and transformation, LOPSTR 2010, held in Hagenberg, Austria in July 2010. the 13 revi...
详细信息
ISBN:
(数字)9783642205514
ISBN:
(纸本)9783642205507
this book constitutes the thoroughly refereed post-proceedings of the 20thinternationalsymposium on logic-basedprogramsynthesis and transformation, LOPSTR 2010, held in Hagenberg, Austria in July 2010. the 13 revised full papers presented together with two invited papers were carefully reviewed and selected from 26 submissions. Among the topics covered are specification, synthesis, verification, analysis, optimization, specialization, security, certification, application and tools, program/model manipulation, and transformation techniques for any programming language paradigm.
this work presents a static analysis technique based on program slicing for CSP specifications. Given a particular event in a CSP specification, our technique allows us to know what parts of the specification must nec...
详细信息
ISBN:
(纸本)9783642005145
this work presents a static analysis technique based on program slicing for CSP specifications. Given a particular event in a CSP specification, our technique allows us to know what parts of the specification must necessarily be executed before this event, and what parts of the specification could be executed before it in some execution. Our technique is based on a new data structure which extends the Synchronized Control Flow Graph (SCFG). We show that this new data structure improves the SCFG by taking into account the context in which processes are called and, thus, makes the slicing process more precise.
the proceedings contain 11 papers. the topics discussed include: space invading systems code;test data generation of bytecode by CLP partial evaluation;a modular equational generalization algorithm;a transformational ...
the proceedings contain 11 papers. the topics discussed include: space invading systems code;test data generation of bytecode by CLP partial evaluation;a modular equational generalization algorithm;a transformational approach to polyvariant BTA of higher-order functional programs;analysis of linear hybrid systems in CLP;automatic generation of test inputs for mercury;analytical inductive functional programming;the MEB and CEB static analysis for CSP specifications;fast offline partial evaluation of large logicprograms;an inference algorithm for guaranteeing safe destruction;from monomorphic to polymorphic well-typings and beyond;and on negative unfolding in the answer set semantics.
this book constitutes the thoroughly refereed post-conference proceedings of the 28thinternationalsymposium on logic-basedprogramsynthesis and transformation, LOPSTR 2018, held in Frankfurt/Main, Germany, in Septe...
详细信息
ISBN:
(数字)9783030138387
ISBN:
(纸本)9783030138370
this book constitutes the thoroughly refereed post-conference proceedings of the 28thinternationalsymposium on logic-basedprogramsynthesis and transformation, LOPSTR 2018, held in Frankfurt/Main, Germany, in September 2018.;the 11 revised full papers were carefully reviewed and selected from 29 submissions. In addition to the 11 papers, this volume includes 3 abstracts of invited talks and 2 abstracts of invited tutorials. the papers are grouped into the following topics: analysis of term rewriting; logic-based distributed/concurrent programming; analysis of logicprogramming; and program analysis.
Computational systems based on a first-order language that can be given a canonical model which captures provability in the corresponding calculus can often be seen as first-order theories S, and computational propert...
详细信息
ISBN:
(纸本)9783319944609;9783319944593
Computational systems based on a first-order language that can be given a canonical model which captures provability in the corresponding calculus can often be seen as first-order theories S, and computational properties of such systems can be formulated as first-order sentences. that hold in such a canonical model of S. In this setting, standard results regarding the preservation of satisfiability of different classes of first-order sentences yield a number of interesting applications in program analysis. In particular, properties expressed as existentially quantified boolean combinations of atoms (for instance, a set of unification problems) can then be disproved by just finding an arbitrary model of the considered theory plus the negation of such a sentence. We show that rewriting-based systems fit into this approach. Many computational properties (e.g., infeasibility and non-joinability of critical pairs in (conditional) rewriting, non-loopingness, or the secure access to protected pages of a web site) can be investigated in this way. Interestingly, this semantic approach succeeds when specific techniques developed to deal withthe aforementioned problems fail.
Fuzzy logicprogramming is a growing declarative paradigm aiming to integrate fuzzy logic into logicprogramming. One of the most difficult tasks when specifying a fuzzy logicprogram is determining the right weights ...
详细信息
ISBN:
(纸本)9783319631394;9783319631387
Fuzzy logicprogramming is a growing declarative paradigm aiming to integrate fuzzy logic into logicprogramming. One of the most difficult tasks when specifying a fuzzy logicprogram is determining the right weights for each rule, as well as the most appropriate fuzzy connectives and operators. In this paper, we introduce a symbolic extension of fuzzy logicprograms in which some of these parameters can be left unknown, so that the user can easily see the impact of their possible values. Furthermore, given a number of test cases, the most appropriate values for these parameters can be automatically computed. Finally, we show some benchmarks that illustrate the usefulness of our approach.
this book presents the thoroughly refereed post-workshop proceedings of the 8thinternational Workshop on logic-basedprogramsynthesis and transformation, LOPSTR'98 held in Manchester, UK in June 1998. the 16 rev...
详细信息
ISBN:
(数字)9783540489580
ISBN:
(纸本)9783540657651
this book presents the thoroughly refereed post-workshop proceedings of the 8thinternational Workshop on logic-basedprogramsynthesis and transformation, LOPSTR'98 held in Manchester, UK in June 1998. the 16 revised full papers presented were carefully reviewed and selected during three rounds of inspection from a total of initially 36 extended abstracts submitted. Also included are eight short papers. Among the topics covered are logic specification, mathematical program construction, logicprogramming, computational logics, inductive programsynthesis, constraint logicprograms, and mathematical foundations.
暂无评论