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 15 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Trace Analysis Using an Event-Driven Interval Temporal logic;the Prol...
ISBN:
(纸本)9783030452599
the proceedings contain 15 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Trace Analysis Using an Event-Driven Interval Temporal logic;the Prolog Debugger and Declarative programming;a Port Graph Rewriting Approach to Relational Database Modelling;Generalization-Driven Semantic Clone Detection in CLP;semi-inversion of Conditional Constructor Term Rewriting Systems;a General Framework for Static Cost Analysis of Parallel logicprograms;incremental Analysis of logicprograms with Assertions and Open Predicates;computing Abstract Distances in logicprograms;synthesizing Imperative Code from Answer Set programming Specifications;verified Construction of Fair Voting Rules;solving Proximity Constraints;a Certified Functional Nominal C-Unification Algorithm;modeling and Reasoning in Event Calculus Using Goal-Directed Constraint Answer Set programming.
the proceedings contain 11 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Multivariant Assertion-based Guidance in Abstract Interpretation;guid...
ISBN:
(纸本)9783030138370
the proceedings contain 11 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Multivariant Assertion-based Guidance in Abstract Interpretation;guided Unfoldings for Finding Loops in Standard Term Rewriting;homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms;multiparty Classical Choreographies;a Pragmatic, Scalable Approach to Correct-by-Construction Process Composition Using Classical Linear logic Inference;Confluence of CHR Revisited: Invariants and Modulo Equivalence;compiling Control as Offline Partial Deduction;predicate Specialization for Definitional Higher-Order logicprograms;an Assertion Language for Slicing Constraint logic Languages.
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.
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.
programsynthesis offers an attractive alternative to the intricate and tedious process of writing assembly programs manually. Assembly programsynthesis automatically generates implementations, given a high-level for...
详细信息
ISBN:
(纸本)9783031712937;9783031712944
programsynthesis offers an attractive alternative to the intricate and tedious process of writing assembly programs manually. Assembly programsynthesis automatically generates implementations, given a high-level formal specification and a machine description. However, its limited scalability prevents widespread adoption. Automatic parallelization improves programsynthesis in general, but parallelizing assembly synthesis is nontrivial as the realities that data are untyped and all state is global lead to an enormous search space and prevent straightforward decomposition into separable sub-problems that can be run in parallel. We present PASSES, a Parallel Assembly synthesis System Exploiting Subspaces. PASSES uses five heuristics to transform an original assembly synthesis problem into a set of sub-problems;it runs multiple synthesis sub-problems in parallel and constructs the final result by combining them. We evaluate PASSES on 26 general bit manipulation assembly programming problems and 140 machine-dependent use cases from two operating systems. Compared to an existing assembly synthesis tool and a state-of-the-art parallel SMT solver, all five heuristics in PASSES significantly improve assembly synthesis scalability.
Propositional simplification and preprocessing are of key importance in the fields of automated reasoning and theorem proving. We present a novel propositional formula representation able to capture all of its n-ary i...
详细信息
ISBN:
(纸本)9783031712937;9783031712944
Propositional simplification and preprocessing are of key importance in the fields of automated reasoning and theorem proving. We present a novel propositional formula representation able to capture all of its n-ary implication information in a tractable manner. From the exploration of this novel encoding in the form of a directed hypergraph, we derive a novel simplification rule which is guaranteed to be equivalencepreserving, monotonically decreasing in the size of the problem, and capable of deep inference. We are not aware of any such generic preprocessing framework capable of systematically simplifying propositional problems in arbitrary form. Interestingly, our rule effectively generalises and streamlines most of the known equivalence-preserving SAT preprocessing techniques. Additionally, since our problem transformations are domain- and application-independent, they can be used in combination with any propositional-logic-based techniques, including those currently used in automated reasoning, solving and optimisation tools.
Various program verification problems for functional programs can be reduced to the validity checking problem for formulas of a fixpoint logic. Recently, Kobayashi et al. have shown that the unfold/fold transformation...
详细信息
ISBN:
(数字)9783030994617
ISBN:
(纸本)9783030994600;9783030994617
Various program verification problems for functional programs can be reduced to the validity checking problem for formulas of a fixpoint logic. Recently, Kobayashi et al. have shown that the unfold/fold transformation originally developed for logicprogramming can be extended and applied to prove the validity of fixpoint logic formulas. In the present paper, we refine their unfold/fold transformation, so that each predicate can be unfolded a different number of times in an asynchronous manner. Inspired by the work of Lee et al. on size change termination, we use a variant of size change graphs to find an appropriate number of unfoldings of each predicate. We have implemented an unfold/fold transformation tool based on the proposed method, and evaluated its effectiveness.
the proceedings contain 15 papers. the special focus in this conference is on Functional and logicprogramming. the topics include: Explanations as programs in Probabilistic logicprogramming;FOLD-R++: A Scalable Tool...
ISBN:
(纸本)9783030994600
the proceedings contain 15 papers. the special focus in this conference is on Functional and logicprogramming. the topics include: Explanations as programs in Probabilistic logicprogramming;FOLD-R++: A Scalable Toolset for Automated Inductive Learning of Default theories from Mixed Data;a Lazy Desugaring System for Evaluating programs with Sugars;on Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs;improving Type Error Reporting for Type Classes;asynchronous Unfold/Fold transformation for Fixpoint logic;programlogic for Higher-Order Probabilistic programs in Isabelle/HOL;generating C: System Description;translation Certification for Smart Contracts;zipping Strategies and Attribute Grammars;unified program Generation and Verification: A Case Study on Number-theoretic Transform;scheduling Complexity of Interleaving Search;preface.
the proceedings contain 20 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Partial evaluation of order-sorted equational programs modulo axioms;...
ISBN:
(纸本)9783319631387
the proceedings contain 20 papers. the special focus in this conference is on logic-basedprogramsynthesis and transformation. the topics include: Partial evaluation of order-sorted equational programs modulo axioms;a formal, resource consumption-preserving translation of actors to Haskell;verification of time-aware business processes using constrained horn clauses;minizinc with strings;slicing concurrent constraint programs;a new functional-logic compiler for curry;symbolic execution and thresholding for efficiently tuning fuzzy logicprograms;hierarchical shape abstraction for analysis of free list memory allocators;a productivity checker for logicprogramming;symbolic abstract contract synthesis in a rewriting framework;on the completeness of selective unification in concolic testing of logicprograms;deriving efficient generators for closed simply-typed lambda terms and normal forms;a reversible semantics for erlang;scaling bounded model checking by transforming programs with arrays;intuitionistic logicprogramming for SQL;coinductive soundness of corecursive type class resolution;nominal unification of higher order expressions with recursive let and automata theory approach to predicate intuitionistic logic.
暂无评论