the proceedings contain 15 papers. the topics discussed include: three syntactic theories for combinatory graph reduction;analysis of air traffic track data withthe AutoBayes synthesis system;proving with ACL2 the co...
ISBN:
(纸本)9783642205507
the proceedings contain 15 papers. the topics discussed include: three syntactic theories for combinatory graph reduction;analysis of air traffic track data withthe AutoBayes synthesis system;proving with ACL2 the correctness of simplicial sets in the Kenzo system;graph generation to statically represent CSP processes;verification of the Schorr-Waite algorithm - from trees to graphs;compositional CLP-based test data generation for imperative languages;on inductive proofs by extended unfold/fold transformation rules;non-termination analysis of logicprograms using types;scaling up algorithmic debugging with virtual execution trees;program specialization for verifying infinite state systems: an experimental evaluation;dependency triples for improving termination analysis of logicprograms with cut;a hybrid approach to conjunctive partial evaluation of logicprograms;and abstract diagnosis of first order functional logicprograms.
the proceedings contains 11 papers. the topics discussed include: declarative programming with function patterns;transformational verification of parameterized protocols using array formulas;an algorithm for local var...
详细信息
ISBN:
(纸本)3540326545
the proceedings contains 11 papers. the topics discussed include: declarative programming with function patterns;transformational verification of parameterized protocols using array formulas;an algorithm for local variable elimination normal logicprograms;removing superfluous versions in polyvariant specialization of prolog programs;extension of type-based approach to generation of stream-processing programs by automatic insertion of buffering primitives;non-leftmost unfolding in partial evaluation of logicprograms with impure predicates;a transformational semantics of static embedded implications of normal logicprograms;converting one type-based abstract domain to another;and experiments in context-sensitive analysis of modular programs.
the proceedings contain 19 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Analysis of rewriting-based systems as first-order theories;a constru...
ISBN:
(纸本)9783319944593
the proceedings contain 19 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Analysis of rewriting-based systems as first-order theories;a constructor-based reachability logic for rewrite theories;fuzzy unification and generalization of first-order terms over similar signatures;nominal C-unification;on uniquely closable and uniquely typable skeletons of Lambda terms;a certified reference validation mechanism for the permission model of android;predicate pairing with abstraction for relational verification;variant-based decidable satisfiability in initial algebras with predicates;combining static and dynamic contract checking for curry;a rule-based approach to analyzing database schema objects with datalog;deadlock detection of java bytecode;inferring energy bounds via static program analysis and evolutionary modeling of basic blocks;CARET analysis of multithreaded programs;context generation from formal specifications for C analysis tools;liveness-driven random program generation;erlang code evolution control;justifications in constraint handling rules for logical retraction in dynamic algorithms.
the proceedings contain 13 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Deciding Knowledge Problems Modulo Classes of Permutative theori...
ISBN:
(纸本)9783031712937
the proceedings contain 13 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Deciding Knowledge Problems Modulo Classes of Permutative theories;binary Implication Hypergraphs for the Representation and Simplification of Propositional Formulae;combined Abstract Congruence Closure for theories with Associativity or Commutativity;a Certifying Algorithm for Linear (and Integer) Feasibility in Horn Constraint Systems;pick a Flavour: Towards Sustainable Deployment of Cloud-Edge Applications;an Axiomatic Category-based Access Control Model for Smart Homes;towards Specification-Guarded Refactoring;impact and Performance of Randomized Test-Generation Using Prolog;proving Uniqueness of Normal Forms w.r.t Reduction of Term Rewriting Systems;rewriting Induction for Higher-Order Constrained Term Rewriting Systems;introducing Quantification into a Hierarchical Graph Rewriting Language.
the proceedings contain 22 papers. the special focus in this conference is on Semantics of logic Languages and Efficient Compilation of Functional logicprograms. the topics include: Proof checking and logicprogrammi...
ISBN:
(纸本)9783319274355
the proceedings contain 22 papers. the special focus in this conference is on Semantics of logic Languages and Efficient Compilation of Functional logicprograms. the topics include: Proof checking and logicprogramming;on dual programs in co-logicprogramming;equational formulas and pattern operations in initial order-sorted algebras;compiling collapsing rules in certain constructor systems;from boolean equalities to constraints;a type-theoretic approach to resolution;a typed language for events;applying sorting networks to synthesize optimized sorting libraries;impact of accuracy optimization on the convergence of numerical iterative methods;abstract analysis of universal properties for TCCP;a global occurrence counting analysis for brane calculi;using dynamic pushdown networks to automate a modular information-flow analysis;checking java assertions using automated test-case generation;a generic intermediate representation for verification condition generation;combining top-down and bottom-up techniques in program derivation;a generalized model for algorithmic debugging;concolic execution in functional programming by program instrumentation;memory policy analysis for semantics specifications in maude;correctness of context-moving transformations for term rewriting systems and CHR in action.
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.
programtransformation and in particular partial evaluation are appealing techniques for declarative programs to improve not only their performance. this paper presents the first step towards developing program transf...
详细信息
ISBN:
(纸本)3540266550
programtransformation and in particular partial evaluation are appealing techniques for declarative programs to improve not only their performance. this paper presents the first step towards developing programtransformation techniques for a concurrent constraint programming language where guarded rules rewrite and augment multi-sets of atomic formulae, called Constraint Handling Rules (CHR). We study the specialization of rules with regard to a given goal (query). We show the correctness of this programtransformation: Adding and removing specialized rules in a program does not change the program's operational semantics. Furthermore termination and confluence of the program are shown to be preserved.
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of programsynthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number ...
详细信息
ISBN:
(纸本)3540266550
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of programsynthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number of program fragments of this chosen typing, using functions and values available in the given typing environment. We call this problem term enumeration,. To solve the problem, we use the Curry-Howard correspondence (propositions-as-types, proofs-as-programs) to transform it into a proof enumeration problem for an intuitionistic logic calculus. We formally study proof enumeration and counting in this calculus. We prove that proof counting is solvable and give an algorithm to solve it. this in turn yields a proof enumeration algorithm.
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.
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.
暂无评论