In this paper, we study termination properties of input-consuming derivations of moded logicprograms. Input-consuming derivations can be used to model the behavior of logicprograms using dynamic scheduling and emplo...
详细信息
the goal of automated programsynthesis is to bridge the gap between what is easy for people to describe and what is possible to execute on a computer. In this paper, we present a framework for synthesis of rule-based...
ISBN:
(纸本)3540404384
the goal of automated programsynthesis is to bridge the gap between what is easy for people to describe and what is possible to execute on a computer. In this paper, we present a framework for synthesis of rule-based solvers for constraints given their logical specification. this approach takes advantage of the power of tabled resolution for constraint logicprogramming, in order to check the validity of the rules. Compared to previous work [8,19,2,5,3], where different methods for automatic generation of constraint solvers have been proposed, our approach enables the generation of more expressive rules (even recursive and splitting rules).
Over the last decade I have worked with colleagues on different projects to develop, implement, and automate the use of calculi for programsynthesis and transformation. these projects had different motivations and go...
详细信息
Scientists and engineers face recurring problems of constructing, testing and modifying numerical simulation programs. the process of coding and revising such simulators is extremely time-consuming, because they are a...
ISBN:
(纸本)3540678395
Scientists and engineers face recurring problems of constructing, testing and modifying numerical simulation programs. the process of coding and revising such simulators is extremely time-consuming, because they are almost always written in conventional programming languages. Scientists and engineers can therefore benefit from software that facilitates construction of programs for simulating physical systems. Our research adapts the methodology of deductive programsynthesis to the problem of constructing numerical simulation codes. We have focused on simulators that can be represented as second order functional programs composed of numerical integration and root extraction routines. We have developed a system that uses first order Horn logic to synthesize numerical simulators built from these components. Our approach is based on two ideas: First, we axiomatize only the relationship between integration and differentiation. We neither attempt nor require a complete axiomatization of mathematical analysis. Second, our system uses a representation in which functions are reified as objects. Function objects are encoded as lambda expressions. Our knowledge base includes an axiomatization of term equality in the lambda calculus. It also includes axioms defining the semantics of numerical integration and root extraction routines. We use depth bounded SLD resolution to construct proofs and synthesize programs. Our system has successfully constructed numerical simulators for computational design of jet engine nozzles and sailing yachts, among others. Our results demonstrate that deductive synthesis techniques can be used to construct numerical simulation programs for realistic applications [EM98].
Schema-basedprogramsynthesis and transformation techniques tend to be either pragmatic, designed for carrying out real programtransformation or synthesis operations but lacking the logical basis to ensure correctne...
ISBN:
(数字)9783540489580
ISBN:
(纸本)3540657657
Schema-basedprogramsynthesis and transformation techniques tend to be either pragmatic, designed for carrying out real programtransformation or synthesis operations but lacking the logical basis to ensure correctness of the programs they synthesise/transform, or rigorous, with strong theoretical foundations, but generating proof obligations which are difficult to satisfy.
the proceedings contain 19 papers. the special focus in this conference is on logicprogramsynthesis and transformation. the topics include: Preserving characteristic trees without constraints;memoing evaluation by s...
ISBN:
(纸本)3540609393
the proceedings contain 19 papers. the special focus in this conference is on logicprogramsynthesis and transformation. the topics include: Preserving characteristic trees without constraints;memoing evaluation by source-to-source transformation;transformation of left terminating programs;derivation of concurrent algorithms in tempo;an argumentation-theoretic approach to logicprogramtransformation;complexity of horn programs;studying the cost of logic languages in an abstract interpretation framework for granularity analysis;ideal refinement of datalog programs;guiding program development systems by a connection based proof strategy;towards an object-oriented methodology for deductive synthesis of logicprograms;logicprogramsynthesis by induction over horn clauses;logicprogramtransformationthrough generalization schemata;an opportunistic approach for logicprogram analysis and optimisation using enhanced schema-basedtransformations;solving deductive planning problems using program analysis and transformation;towards a complete proof procedure to prove properties of normal logicprograms under the completion;termination of logicprograms using semantic unification;on the mechanics of metasystem hierarchies in programtransformation and efficient translation of lazy functional logicprograms into prolog.
the proceedings contain 25 papers. the special focus in this conference is on programming. the topics include: Procedures and concurrency: A study in proof;another characterization of weakest preconditions;powerdomain...
ISBN:
(纸本)9783540114949
the proceedings contain 25 papers. the special focus in this conference is on programming. the topics include: Procedures and concurrency: A study in proof;another characterization of weakest preconditions;powerdomains and nondeterministic recursive definitions;optimizing for a multiprocessor: Balancing synchronization costs against parallelism in straight-line code;the simple semantics for Coppo-Dezani-Sallé types;proving the correctness of implementations of shared data abstractions;specification of communicating processes and process implementation correctness;a system for reasoning within and about algebraic specifications;tuning algebraic specifications by type merging;a machine-level semantics for nondeterministic, parallel programs;communicating agents for applicative concurrent programming;on effective computations of non-deterministic schemes;Specification and verification of concurrent systems in CESAR;proof of separability A verification technique for a class of security kernels;a method for programsynthesis;the use of transformations to implement an algorithm;a formalized proof system for total correctness of while programs;automatic programtransformation viewed as theorem proving;an enlarged definition and complete axiomatization of observational congruence of finite processes;perluette : A compilers producing system using abstract data types;a weakest precondition semantics for communicating processes;from abstract model to efficient compilation of patterns;computer-basedsynthesis of logicprograms.
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 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.
this book constitutes the refereed proceedings of the 15thinternationalsymposium on Static Analysis, SAS 2008, held in Valencia, Spain in July 2008 - co-located with LOPSTR 2008, the internationalsymposium on logic...
详细信息
ISBN:
(数字)9783540691662
ISBN:
(纸本)9783540691631
this book constitutes the refereed proceedings of the 15thinternationalsymposium on Static Analysis, SAS 2008, held in Valencia, Spain in July 2008 - co-located with LOPSTR 2008, the internationalsymposium on logic-basedprogramsynthesis and transformation, PPDP 2008, the international ACM SIGPLAN symposium on Principles and Practice of Declarative programming, and PLID 2008, the international Workshop on programming Language Interference and Dependence. the 22 revised full papers presented together with two invited lectures were carefully reviewed and selected from 63 submissions. the papers address all aspects of static analysis including abstract domains, abstract interpretation, abstract testing, compiler optimizations, control flow analysis, data flow analysis, model checking, program specialization, security analysis, theoretical analysis frameworks, type based analysis, and verification systems.
暂无评论