LEADER 05107nam 2200493 450 001 996490364303316 005 20230208015008.0 010 $a9783031167676$b(electronic bk.) 010 $z9783031167669 035 $a(MiAaPQ)EBC7084588 035 $a(Au-PeEL)EBL7084588 035 $a(CKB)24819545400041 035 $a(PPN)264953193 035 $a(EXLCZ)9924819545400041 100 $a20230208d2022 uy 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 00$aLogic-based program synthesis and transformation $e32nd International Symposium, LOPSTR 2022, Tbilisi, Georgia, September 21-23, 2022, proceedings /$fAlicia Villanueva (editor) 210 1$aCham, Switzerland :$cSpringer,$d[2022] 210 4$d©2022 215 $a1 online resource (165 pages) 225 1 $aLecture notes in computer science ;$v13474 311 08$aPrint version: Villanueva, Alicia Logic-Based Program Synthesis and Transformation Cham : Springer International Publishing AG,c2022 9783031167669 320 $aIncludes bibliographical references and index. 327 $aIntro -- 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. 327 $a5 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. 410 0$aLecture notes in computer science ;$v13474. 606 $aComputer logic 606 $aComputer logic$vCongresses 606 $aComputer software$xDevelopment 615 0$aComputer logic. 615 0$aComputer logic 615 0$aComputer software$xDevelopment. 676 $a004.015113 702 $aVillanueva$b Alicia 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 912 $a996490364303316 996 $aLogic-Based Program Synthesis and Transformation$92804552 997 $aUNISA