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.
the proceedings contain 19 papers. the special focus in this conference is on Practical Aspects of Declarative Languages. the topics include: From Starvation Freedom to All-Path Reachability Problems in Cons...
ISBN:
(纸本)9783031248405
the proceedings contain 19 papers. the special focus in this conference is on Practical Aspects of Declarative Languages. the topics include: From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting;switchLog: A logicprogramming Language for Network Switches;linear Algebraic Abduction with Partial Evaluation;Using Hybrid Knowledge Bases for Meta-reasoning over OWL 2 QL;solving Vehicle Equipment Specification Problems with Answer Set programming;UAV Compliance Checking Using Answer Set programming and Minimal Explanations Towards Compliance (Application Paper);jury-Trial Story Construction and Analysis Using Goal-Directed Answer Set programming;pruning Redundancy in Answer Set Optimization Applied to Preventive Maintenance Scheduling;automatic Rollback Suggestions for Incremental Datalog Evaluation;programsynthesis Using Example Propagation;embedding Functional logicprogramming in Haskell via a Compiler Plugin;execution Time program Verification with Tight Bounds;fluo: A Domain-Specific Language for Experiments in Fluorescence Microscopy (Application Paper);flexible Job-shop Scheduling for Semiconductor Manufacturing with Hybrid Answer Set programming (Application Paper);Integrating ASP-based Incremental Reasoning in the Videogame Development Workflow (Application Paper);dynamic Slicing of Reaction Systems based on Assertions and Monitors;multiple Query Satisfiability of Constrained Horn Clauses.
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.
the proceedings contain 24 papers. the special focus in this conference is on Automated Technology for Verification and Analysis. the topics include: Live synthesis;faster Pushdown Reachability Analysis with Applicati...
ISBN:
(纸本)9783030888848
the proceedings contain 24 papers. the special focus in this conference is on Automated Technology for Verification and Analysis. the topics include: Live synthesis;faster Pushdown Reachability Analysis with Applications in Network Verification;verifying Verified Code;probabilistic Causes in Markov Chains;TEMPEST - synthesis Tool for Reactive Systems and Shields in Probabilistic Environments;AQUA: Automated Quantized Inference for Probabilistic programs;Proving SIFA Protection of Masked Redundant Circuits;verification by Gambling on program Slices;runtime Enforcement of Hyperproperties;determinization and Limit-Determinization of Emerson-Lei Automata;compositional synthesis of Modular Systems;event-B Refinement for Continuous Behaviours Approximation;incorporating Monitors in Reactive synthesis Without Paying the Price;pyNeVer: A Framework for Learning and Verification of Neural Networks;property-Directed Verification and Robustness Certification of Recurrent Neural Networks;automatic Discovery of Fair Paths in Infinite-State Transition Systems;Certifying DFA Bounds for Recognition and Separation;AALpy: An Active Automata Learning Library;Learning Linear Temporal Properties from Noisy Data: A MaxSAT-based Approach;mining Interpretable Spatio-Temporal logic Properties for Spatially Distributed Systems;A Formal Semantics of the GraalVM Intermediate Representation;A Verified Decision Procedure for Orders in Isabelle/HOL.
暂无评论