Rewriting Logic and Its Applications 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018, Proceedings. Theoretical Computer Science and General Issues

This book constitutes revised selected papers from the 12th International Workshop on Rewriting Logic and Its Applications, WRLA 2018, held in Thessaloniki, Greece, in June 2018. The 12 full papers presented in this volume were carefully reviewed and selected from 21 submissions. They deal with rewriting, a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction, and its applications. Preface 6 Organization 8 Automata and Equations Based Approximations for Reachability Analysis (Invited Talk) 9 Contents 11 Benchmarking Implementations of Term Rewriting and Pattern Matching in Algebraic, Functional, and Object-Oriented Languages 13 1 Introduction 13 2 Selected Tools 15 3 The REC-2017 Language 16 4 The REC-2017 Translators 19 5 Selected Benchmarks 23 6 Language Conciseness 25 7 Execution Platform 27 8 Experimental Results 29 9 Threats to Validity 31 10 Conclusion 33 References 35 Multi-paradigm Programming in Maude 38 1 Introduction 38 2 Example: Missionaries and Cannibals 41 3 Background on Rewriting Logic and Term Rewriting 42 4 Narrowing in Maude 45 4.1 The Variant Narrowing Strategy 48 4.2 The Folding Variant Narrowing Strategy 48 4.3 Variant-Based Unification in Maude 2.7.1 49 5 Missionaries and Cannibals Using Symbolic Reachability 49 6 Missionaries and Cannibals Using Variant Equations 52 7 Conclusions 53 References 54 MUnit: A Unit Framework for Maude 57 1 Introduction 57 2 MUnit 59 3 Running Example 60 4 Implementation 66 5 Related Work 67 6 Conclusions and Ongoing Work 68 References 69 Parameterized Programming for Compositional System Specification 71 1 Introduction 71 2 A Primer on Parameterized Programming and Maude 73 3 A Primer on Synchronous Composition and Egalitarian Maude 74 4 Parameterized Programming for System Specification 77 5 Example: Alternating Bit Protocol 80 6 Guarantees, Assumptions, and Compositional Verification 84 7 Related Work 85 8 Concluding Remarks 86 References 86 Symbolic Specification and Verification of Data-Aware BPMN Processes Using Rewriting Modulo SMT 88 1 Introduction 88 2 BPMN with Data 90 3 Rewriting Logic and Rewriting Modulo SMT in a Nutshell 93 4 Symbolic Specification 95 5 Symbolic Execution and Reachability Analysis 99 5.1 Symbolic Rewriting 100 5.2 Symbolic Reachability Analysis 100 6 Related Work 105 7 Concluding Remarks 106 References 107 Associative Unification and Symbolic Reasoning Modulo Associativity in Maude 110 1 Introduction 110 2 The Associative Unification Algorithm in Maude 112 2.1 The pig-pug procedure 113 2.2 Forcing Termination 114 2.3 Combining Unification Algorithms 115 3 Built-In Order-Sorted Unification Modulo Axioms 115 4 Built-In Variant Generation 117 5 Built-In Variant-Based Unification 119 6 Narrowing-Based Symbolic Reachability Analysis 120 7 Conclusions and Related Work 123 References 124 Proving Structural Properties of Sequent Systems in Rewriting Logic 127 1 Introduction 127 2 Three Structural Properties of Sequent-Based Logics 129 3 Rewriting Logic Preliminaries 132 4 Checking Admissibility, Invertibility, and Permutability 133 5 Reflective Implementation 136 5.1 Sequent System Specification 136 5.2 Property Specification 138 5.3 The Algorithms 139 6 Case Studies 140 6.1 System G3ip 140 6.2 Multi-conclusion Propositional Intuitionistic Logic (mLJ) 142 6.3 Propositional Classical Logic (G3cp) 142 6.4 Linear Logic (LL) 143 6.5 Normal Modal Logics: K and S4 144 7 Related Work and Concluding Remarks 145 References 146 Formal Modeling and Analysis of the Walter Transactional Data Store 148 1 Introduction 148 2 Preliminaries 150 3 A Formal Model of Walter in Maude 153 4 Correctness Analysis 156 4.1 Parametric Generation of Initial States 156 4.2 Analyzing the Correctness Properties 156 5 Performance Estimation by Statistical Model Checking 159 6 Related Work 162 7 Conclusions 162 References 163 Extending Timbuk to Verify Functional Programs 165 1 Motivations 165 2 Simplified Regular Tree Expressions 166 3 The Need for Abstraction Equations 168 4 Generating Abstraction Equations Ec 169 5 Interacting with Timbuk 170 6 Conclusion and Further Research 172 References 174 Generalized Rewrite Theories and Coherence Completion 176 1 Introduction 176 2 Preliminaries on Order-Sorted Algebra and Variants 177 3 Generalized Rewrite Theories and Coherence 182 4 Coherence Completion of Generalized Rewrite Theories 186 5 Related Work and Conclusions 193 References 194 Proving Ground Confluence of Equational Specifications Modulo Axioms 196 1 Introduction 196 2 Preliminaries 198 3 An Equational Specification for Hereditarily Finite Sets 200 4 Proving Ground Joinability 204 5 Ground Convergence of HF-SETS 211 6 Related Work and Conclusion 214 References 215 Uniform Strong Normalization for Multi-discipline Calculi 217 1 Introduction 217 2 A Language Approach to Abstract Machines 219 3 Substitution Disciplines 222 4 A Parametric, Multi-discipline Sequent Calculus 224 5 Strong Normalization 227 6 Biorthogonals are Fixed Points 233 7 Conclusion 235 References 236 Real-Time Rewriting Logic Semantics for Spatial Concurrent Constraint Programming 238 1 Introduction 238 2 Preliminaries 240 3 Rewriting Logic Semantics 242 3.1 System States 242 3.2 Commands 244 3.3 Time Scaffolding 245 3.4 The Constraint System 247 3.5 System Transitions 247 4 Reachability Analysis 250 5 Related Work and Concluding Remarks 253 References 255 Approximating Any Logic Program by a CS-Program 257 1 Introduction 257 2 Preliminaries 258 2.1 Resolution 259 2.2 CS-Program 259 2.3 Transforming Any Logic Program into a CS-Program 260 3 Making the Limet-Salzer Technique LSspsJAR06 Terminate 262 3.1 Generalization 263 3.2 Integration of Generalization in LSspsJAR06 264 3.3 Results 264 4 Example 268 5 Discussion 271 6 Conclusion 271 References 272 Author Index 273 Front Matter ....Pages I-XII Benchmarking Implementations of Term Rewriting and Pattern Matching in Algebraic, Functional, and Object-Oriented Languages (Hubert Garavel, Mohammad-Ali Tabikh, Imad-Seddik Arrada)....Pages 1-25 Multi-paradigm Programming in Maude (Santiago Escobar)....Pages 26-44 MUnit: A Unit Framework for Maude (Adrián Riesco)....Pages 45-58 Parameterized Programming for Compositional System Specification (Óscar Martín, Alberto Verdejo, Narciso Martí-Oliet)....Pages 59-75 Symbolic Specification and Verification of Data-Aware BPMN Processes Using Rewriting Modulo SMT (Francisco Durán, Camilo Rocha, Gwen Salaün)....Pages 76-97 Associative Unification and Symbolic Reasoning Modulo Associativity in Maude (Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Carolyn Talcott)....Pages 98-114 Proving Structural Properties of Sequent Systems in Rewriting Logic (Carlos Olarte, Elaine Pimentel, Camilo Rocha)....Pages 115-135 Formal Modeling and Analysis of the Walter Transactional Data Store (Si Liu, Peter Csaba Ölveczky, Qi Wang, José Meseguer)....Pages 136-152 Extending Timbuk to Verify Functional Programs (Thomas Genet, Tristan Gillard, Timothée Haudebourg, Sébastien Lê Cong)....Pages 153-163 Generalized Rewrite Theories and Coherence Completion (José Meseguer)....Pages 164-183 Proving Ground Confluence of Equational Specifications Modulo Axioms (Francisco Durán, José Meseguer, Camilo Rocha)....Pages 184-204 Uniform Strong Normalization for Multi-discipline Calculi (Paul Downen, Philip Johnson-Freyd, Zena M. Ariola)....Pages 205-225 Real-Time Rewriting Logic Semantics for Spatial Concurrent Constraint Programming (Sergio Ramírez, Miguel Romero, Camilo Rocha, Frank Valencia)....Pages 226-244 Approximating Any Logic Program by a CS-Program (Yohan Boichut, Vivien Pelletier, Pierre Réty)....Pages 245-260 Back Matter ....Pages 261-261