Logic-Based Program Synthesis and Transformation: 30th International Symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020, Proceedings (Theoretical Computer Science and General Issues)

This book constitutes the refereed proceedings of the 30 th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020, which was held during September 7-9, 2020. The 15 papers presented in this volume were carefully reviewed and selected from a total of 31 submissions. The book also contains two invited talks in full paper length. The contributions were organized in topical sections named: rewriting; unification; types; verification; model checking and probabilistic programming; program analysis and testing; and logics. Preface Organization Contents Rewriting Symbolic Computation in Maude: Some Tapas 1 Introduction 1.1 What is Maude? 1.2 Symbolic Computation in Maude 1.3 Tapas and Paper Napkins 2 First Tapas Serving: Rewriting Modulo Axioms B 3 Second Tapas Serving: Unification and Narrowing Modulo B 4 Third Tapas Serving: Variants, and Unification Modulo E B 5 Fourth Tapas Serving: Variant Satisfiability 6 Dessert: Narrowing-Based Symbolic Reachability Analysis 7 Further Reading 7.1 Further Reading on Maude 7.2 Further Background Reading References Runtime Complexity Analysis of Logically Constrained Rewriting 1 Introduction 2 Step by Step to an Optimal Bound 3 Logically Constrained Term Rewriting 4 Complexity Framework 5 Processors 6 Processors for Splitting and Loop Summary 7 Evaluation 8 Conclusion References Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables 1 Introduction 2 Nominal Rewriting Systems with Atom-Variables 2.1 Preliminaries 2.2 Ground Nominal Terms 2.3 Nominal Term Expressions 2.4 Nominal Rewriting Systems with Atom-Variables 2.5 Overlaps and Orthogonality 3 Confluence and Commutation for Left-Linear Nominal Rewriting Systems with Atom-Variables 3.1 Uniformity and -stability 3.2 Parallel Reduction 3.3 Proofs of Commutation and Confluence 4 Conclusion and Related Work References Pattern Eliminating Transformations 1 Introduction 2 Preliminary Notions 3 Pattern-Free Terms and Corresponding Semantics 3.1 Pattern-Free Terms 3.2 Generalized Ground Semantics 3.3 Semantics Preserving CBTRS 4 Deep Semantics for Pattern-Free Properties 4.1 Deep Semantics 4.2 Establishing Pattern-Free Properties 4.3 Establishing Semantics Preserving Properties 5 Related Work 6 Conclusion and Perspectives References Unification Nominal Unification with Letrec and Environment-Variables 1 Introduction 2 Nominal Expressions 3 Nominal Unification with Environments 4 A Decision Algorithm 5 Nonlinear Occurrences of Expression-Variables 6 Conclusion and Future Work References Terminating Non-disjoint Combined Unification 1 Introduction 2 Preliminaries 2.1 Equational Theories 2.2 Equational Term Rewrite Systems 2.3 Forward Closure 3 Hierarchical Unification 3.1 Subterm Collapse-Free Theories 3.2 Forward-Closed E-Constructed TRSs 4 Combined Hierarchical Unification 4.1 Combining Subterm Collapse-Free Theories 4.2 Combining Forward-Closed E-Constructed TRSs 5 Conclusion References Types slepice: Towards a Verified Implementation of Type Theory in Type Theory 1 Introduction 2 Specification 3 Refinement Calculus 4 Decidability of Refinement 5 Proof-Relevant Resolution 6 Related Work 7 Conclusion References Resourceful Program Synthesis from Graded Linear Types 1 Introduction 2 Graded Linear -calculus 3 The Synthesis Calculi 3.1 Subtractive Resource Management 3.2 Additive Resource Management 3.3 Focusing 4 Evaluation 5 Discussion References Verification Reasoning in the Theory of Heap: Satisfiability and Interpolation 1 Introduction 1.1 Encoding Programs Using the Theory of Heap 2 Preliminaries 2.1 The Theory of Heap 2.2 An Interpolating Sequent Calculus for First-Order Logic Modulo Integers 2.3 Reduction for the Theory of Algebraic Data-Types 3 A Decision Procedure for the Theory of Heap 3.1 The Core Language for Heap Formulas 3.2 Translation to the Core Language 3.3 The Sequent Calculus for the Core Language 3.4 Properties of the Calculus 4 Craig Interpolation in the Theory of Heap 5 Related Work 6 Conclusions and Outlook References Algorithm Selection for Dynamic Symbolic Execution: A Preliminary Study 1 Introduction 2 Preliminaries 2.1 Algorithm Selection 2.2 Dynamic Symbolic Execution 3 The AS/DSE Model 3.1 Solver Selection 3.2 Solver Execution 3.3 Solution Selection 3.4 Aggregate Coverage 4 A Preliminary Evaluation 5 Related Work 6 Conclusions References Translation of Interactive Datalog Programs for Microcontrollers to Finite State Machines 1 Introduction 2 Language, State Management, Example Application 3 Computing a Sequence of States 4 Precomputation of States 5 Generating Compact Code for Small Microcontrollers 6 Termination 7 Negation 8 Conclusion References Model Checking and Probabilistic Programming Generating Functions for Probabilistic Programs 1 Introduction 2 Formal Power Series 3 Generating Functions 4 FPS Semantics for pGCL 4.1 FPS Transformer Semantics 4.2 Healthiness Conditions of FPS Transformers 4.3 Embedding into Kozen's Semantics Framework 5 Analysis of Probabilistic Programs 5.1 Invariant-Style Overapproximation of Loops 5.2 Rational PGFs 6 Conclusion References Verification of Multiplayer Stochastic Games via Abstract Dependency Graphs 1 Introduction 2 Turn-Based Stochastic Games 2.1 Definition of Stochastic Games 2.2 Strategies 3 Probabilistic Weighted ATL 4 Model Checking Through Dependency Graphs 4.1 Abstract Dependency Graphs 4.2 The Reduction 5 Implementation and Experimental Evaluation 5.1 Results 6 Conclusion References Program Analysis and Testing Testing Your (Static Analysis) Truths 1 Introduction and Motivation 2 Preliminaries 3 Overview of the Approach 4 The Algorithm 4.1 Basic Reasoning Behind the Approach 4.2 The Algorithm 4.3 Other Details and Observations 5 Applications and Examples 6 A More Detailed Case Study 7 Related Work 8 Conclusions and Future Work References Slicing Unconditional Jumps with Unnecessary Control Dependencies 1 Introduction 2 Unconditional Jumps and the PPDG 3 Alternative Solution: Unnecessary Control Dependencies 4 The Representation of switch Statements 5 Implementation 6 Conclusions References Logics A Formal Model for a Linear Time Correctness Condition of Proof Nets of Multiplicative Linear Logic 1 Introduction 2 Multiplicative Linear Logic, Proof Structures and Proof Nets 2.1 Multiplicative Linear Logic 2.2 MLL Proof Nets 3 The Rewriting System over deNM-Trees 3.1 deNM-Trees 3.2 The Rewriting System over deNM-Trees 4 Linear Time Correctness Condition: A Formal Approach 4.1 Union-Find Data Structures 4.2 Data Specification 4.3 Operational Semantics 5 Concluding Remarks References Synthesis of Modality Definitions and a Theorem Prover for Epistemic Intuitionistic Logic 1 Introduction 2 Overview of Artemov and Protopopescu's IEL logic 3 The G4ip Prover for IPC 3.1 The LJT/G4ip Calculus, (Restricted Here to the Implicational Fragment) 3.2 A Lightweight Theorem Prover for Intuitionistic Propositional Logic 4 The Definition Formula Generator 4.1 Generating Operator Trees 4.2 Synthesizing the Definitions of Modal Operators 5 Discovering the Embedding of IEL and Dosen's Double Negation Modality in IPC 5.1 The Discovery Mechanism for IEL 5.2 Eliminating Dosen's Double Negation Modality 5.3 Knowledge as Awareness? 5.4 The Theorem Prover for IEL 5.5 Discussion 6 Discovering an Embedding of S4 Without the Necessitation Rule 7 Related Work 8 Conclusions References Author Index