Logic-Based Program Synthesis and Transformation: 32nd International Symposium, LOPSTR 2022, Tbilisi, Georgia, September 21–23, 2022, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the 32 nd International Symposium on Logic-Based Synthesis and Transformation, LOPSTR 2022, which was held during September 21-23, 2022. The 8 full papers were selected from 17 submissions and cover different aspects of logic-based program development, all stages of the software life cycle, and issues of both programming-in-the-small and programming-in-the-large. Preface Organization Keynotes Systematic Testing for Robotic Systems Automated Termination and Complexity Analysis Contents Analysis of Rewrite Systems Analysing Parallel Complexity of Term Rewriting 1 Introduction 2 Term Rewriting and Innermost Runtime Complexity 3 Finding Upper Bounds for Parallel Complexity 4 From Parallel DTs to Innermost Rewriting 5 Implementation and Experiments 6 Related Work, Conclusion, and Future Work References Confluence Framework: Proving Confluence with CONFident 1 Introduction 2 Preliminaries 3 Supported Variants of Rewrite Systems 3.1 Logic-Based Description of Rewriting Computations 3.2 Conditional Critical Pairs and Extended -Critical Pairs 3.3 Running Examples 4 Confluence Framework 5 List of Processors 6 Proofs in the Confluence Framework 7 Strategy 8 Structure of CONFident 9 Experimental Results 10 Related Work 11 Conclusions and Future Work References Variant-Based Equational Anti-unification 1 Introduction 2 Preliminaries 3 Least General Anti-unification Modulo Equational Theories via Variant Computation 3.1 Syntactic Anti-unification 3.2 Anti-unification Modulo an Equational Theory 3.3 An Equational Anti-unfication Example 4 Correctness and Completeness of the Equational Anti-unification Algorithm 5 Conclusion A An Application of Equational Generalization to a Biological Domain References Verification and Synthesis Model Checking Meets Auto-Tuning of High-Performance Programs 1 Motivation and Related Work 2 Our Adaptation of Model Checking for Auto-Tuning 3 Our Modeling Approach: From OpenCL to Promela 3.1 An Abstract OpenCL Platform Model 3.2 An Abstract OpenCL Program 4 Using SPIN for Auto-Tuning OpenCL Programs 5 Refining the Counterexample Method for Limited Computation Resources 6 Experimental Results 7 Conclusion References Building a Join Optimizer for Soufflé 1 Introduction 2 Background and Motivating Example 3 A Join Optimizer for Soufflé 3.1 The Profiling Stage 3.2 The Join Ordering Stage 4 Experimental Evaluation 5 Related Work 6 Conclusion References From Infinity to Choreographies 1 Introduction 2 Background 2.1 Networks 2.2 Choreographies 2.3 Extraction Algorithm 3 Networks and Choreographies with Process Spawning 4 Extraction with Process Spawning 4.1 Generating SEGs 4.2 Generating the Choreography 4.3 Implementation and Limitations 5 Conclusion References Logic Programming Typed SLD-Resolution: Dynamic Typing for Logic Programming 1 Introduction 2 Preliminary Concepts 2.1 Three-Valued Logic 2.2 Types 2.3 Terms 2.4 Programs and Queries 3 Typed Unification 4 Operational Semantics 4.1 TSLD-Derivation 4.2 TSLD-Tree 5 Declarative Semantics 5.1 Domains 5.2 Interpretations 5.3 Models 5.4 Type Errors 5.5 Soundness of TSLD-resolution 6 Conclusions and Future Work References On Correctness of Normal Logic Programs 1 Introduction 2 Preliminaries 3 Program Correctness 3.1 Specifications 3.2 Sufficient Condition for Correctness 1 3.3 Sufficient Condition for Correctness 2 4 Correctness for the Well-Founded Semantics 5 Conclusions References Author Index