دانلود کتاب 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)

فهرست مطالب :

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