Recent Trends in Algebraic Development Techniques: 25th International Workshop, WADT 2020, Virtual Event, April 29, 2020, Revised Selected Papers (Lecture Notes in Computer Science, 12669)

Description

This book constitutes the thoroughly refereed post-conference proceedings of the 25th International Workshop on Algebraic Development Techniques, WADT 2020, held virtually in April 2020. The 7 revised papers presented together with an invited paper were carefully reviewed and selected from 9 submissions. The contributed presentations covered a range of topics about the algebraic approach to system specification, which encompasses many aspects of the formal design of software systems. Originally born as formal method for reasoning about abstract data types, the algebraic approach now covers new specification frameworks and programming paradigms (such as object-oriented, aspect-oriented, agent-oriented, logic, and higher-order functional programming) as well as a wide range of application areas (including information systems, concurrent, distributed, and mobile systems). Preface Organization Contents Invited Paper On Completeness of Liveness Synthesis for Parametric Timed Automata (Extended Abstract) 1 Introduction 2 Parametric Timed Automata and Parametric Zones 3 Parameter Synthesis Algorithms 4 Completeness 5 Conclusion References Contributed Papers The Wheel of Rational Numbers as an Abstract Data Type 1 Introduction 2 Preliminaries on ADTs 2.1 The Approach of ADTs 2.2 Arithmetic Structures 3 The Wheel of Rationals 3.1 Basic Constructions with Rationals 3.2 A Wheel of Rationals 4 Initial Algebra Specification of the Wheel of Rationals 4.1 Axioms 4.2 Remarks on the Equations 4.3 Equational Specification Theorem 5 Concluding Remarks References Towards General Axiomatizations for Bisimilarity and Trace Semantics 1 Introduction 2 Background 2.1 The ULTraS Metamodel 2.2 Reachability-Consistent Semirings 2.3 Bisimulation Post-/Pre-metaequivalences 2.4 Resolutions of Nondeterminism 2.5 Reachability Measures 2.6 Coherency-Based Trace Post-/Pre-metaequivalences 3 A Process Algebraic View of ULTraS 4 Axiomatizations of Behavioral Metaequivalences 4.1 Core Axioms: Associativity, Commutativity, Neutral Element 4.2 Equational Characterization of Bpost: Idempotency 4.3 Equational Characterization of Bpre: B-Shuffling 4.4 Equational Characterization of Tpost: Choice Deferral 5 Conclusions References Monographs, a Category of Graph Structures 1 Introduction 2 Notations and Definitions 3 Categories of Monographs 4 Drawing Monographs 5 Monadic Signatures as Monographs 6 Monadic Algebras as Typed Monographs 7 Some Properties of MonoGr 8 Conclusion References Parallel Coherent Graph Transformations 1 Introduction 2 Weak Spans 3 Parallel Coherent Transformations 4 PCTs in the Theory of Adhesive HLR Categories 5 Finitely Attributed Structures 6 Examples 7 Conclusion and Related Work References K and KIV: Towards Deductive Verification for Arbitrary Programming Languages 1 Introduction 1.1 Related Work 2 From K to KIV 2.1 The K Framework 2.2 KIV Proof Assistant 2.3 Syntax and Configuration 2.4 From Rewrite Rules to Axioms 3 One-Path Reachability in KIV 3.1 Configuration Patterns 3.2 One-Path Reachability Properties 3.3 OPR Calculus 4 Reducing Manual Effort 5 Conclusion References Institution-Based Encoding and Verification of Simple UML State Machines in CASL/SPASS 1 Introduction 2 Background on Institutions 2.1 Institutions and Theoroidal Institution Comorphisms 2.2 Casl and the Institution CFOL= 3 Simple UML State Machines 3.1 Event/Data Signatures, Data States and Transitions 3.2 Syntax of Simple UML State Machines 3.3 Event/Data Structures and Models of Simple UML State Machines 3.4 Event/Data Signature Morphisms, Reducts, and Translations 4 A Hybrid Modal Logic for Event/Data Systems 4.1 Formulæ and Sentences of M"3223379 D 4.2 Satisfaction Relation for M"3223379 D 4.3 Representing Simple UML State Machines in M"3223379 D 5 A Theoroidal Comorphism from M"3223379 D to Casl 6 Proving Properties of UML State Machines with HeTS and Spass 6.1 Implementation in HeTS 6.2 Proving in Spass 7 Conclusions and Future Work References Structure-Preserving Diagram Operators 1 Introduction and Related Work 2 Preliminaries 3 Structure-Preserving Diagram Operators 3.1 Motivation: The Pushout Operator 3.2 Linear Operators 3.3 Structure-Preserving Lifting of Linear Operators 3.4 Structure-Preservation of the Lifting 3.5 Composing Operators 4 Applications 4.1 Universal Algebra 4.2 Polymorphic Generalization 5 Conclusion and Future Work References Author Index