Logic-based program synthesis and transformation : 28th International Symposium, LOPSTR 2018, Frankfurt/Main, Germany, September 4-6, 2018, Revised selected papers / Fred Mesnard, Peter J. Stuckey (eds.).

Includes author index.

Online resource; title from PDF title page (SpringerLink, viewed March 27, 2019).

Intro; Preface; Organization; Abstracts of Invited Talks; Formal Methods for JavaScript; Constrained Horn Clauses for Verification; Experiences in Designing Scalable Static Analyses; Abstracts of Invited Tutorials; The VeriMAP System for Program Transformation and Verification; 25 Years of Ciao; Contents; Analysis of Term Rewriting; Proving Program Properties as First-Order Satisfiability; 1 Introduction; 2 Many-Sorted First-Order Logic; 3 Preservation of Many-Sorted First-Order Sentences; 4 Surjective Homomorphisms; 5 Examples of Application with Positive Sentences

5.1 Complete Definedness and Commutativity5.2 Top-Termination; 6 Refutation Witnesses; 7 Example of Application with General Sentences; 8 Related Work; 9 Conclusions and Future Work; References; Guided Unfoldings for Finding Loops in Standard Term Rewriting; 1 Introduction; 2 Preliminaries; 3 Guided Unfoldings; 4 Inferring Terms that Loop; 5 Further Comparisons with the Approach of payet08; 6 Experiments; 7 Conclusion; References; Homeomorphic Embedding Modulo Combinations of Associativity and Commutativity Axioms; 1 Introduction; 2 Preliminaries; 2.1 Pure Homeomorphic Embedding

3 Homeomorphic Embedding Modulo Equational Axioms4 Goal-Driven Homeomorphic Embedding Modulo B; 4.1 An Homeomorphic Embedding Calculus Modulo B; 4.2 Reachability-Based, Goal-Driven Homeomorphic Embedding Formulation; 5 Meta-Level Deterministic Goal-Driven Homeomorphic Embedding Modulo B; 6 Experiments; 7 Concluding Remarks; References; Logic-Based Distributed/Concurrent Programming; Multiparty Classical Choreographies; 1 Introduction; 2 Preview; 3 GCP with Hypersequents; 4 Extending GCP with Choreographies; 5 Projection and Extraction; 6 Related Work and Discussion; References

A Pragmatic, Scalable Approach to Correct-by-Construction Process Composition Using Classical Linear Logic Inference1 Introduction; 2 Background; 2.1 Classical Linear Logic; 2.2 Related Work; 3 Process Specification; 4 Process Composition; 5 Auxiliary Processes; 6 Parallel Composition -- The TENSOR Action; 7 Conditional Composition -- The WITH Action; 8 Sequential Composition -- The JOIN Action; 8.1 Atomic or Matching Output; 8.2 Parallel Output; 8.3 Optional Output; 8.4 Putting It All Together; 9 Conclusion; References; Confluence of CHR Revisited: Invariants and Modulo Equivalence

1 Introduction1.1 Related Work; 1.2 Contributions; 1.3 Overview; 2 Basic Concepts, Confluence, Invariants and Equivalences; 3 Abstract Simulation; 4 Constraint Handling Rules; 4.1 Syntax; 4.2 The Logic-Based Operational Semantics for CHR; 5 Confluence Under the Logic-Based Semantics Re-Explained, and Why Invariants Are Difficult; 6 Invariants and Modulo Equivalence; 6.1 The Choice of a Ground Representation; 7 Conclusion; References; Analysis of Logic Programming; Compiling Control as Offline Partial Deduction; 1 Introduction; 2 Preliminaries; 3 Running Example: Permutation Sort

This book constitutes the thoroughly refereed post-conference proceedings of the 28th International Symposium on Logic-Based Program Synthesis 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 logic programming; and program analysis.