Semantics, Logics, and Calculi
Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays
Published on 7. January 2016
X, 345 pages
978-3-319-27810-0 (ISBN)
Description
This Festschrift volume is published in honor of Hanne Riis Nielson and Flemming Nielson on the occasion of their 60th birthdays in 2014 and 2015, respectively. The papers included in this volume deal with the wide area of calculi, semantics, and analysis.
The book features contributions from colleagues, who have worked together with Hanne and Flemming through their scientific life and are dedicated to them and to their work. The papers were presented at a colloquium at the Technical University of Denmark in January 2016.
Reviews / Votes
"The collection at hand contains a fairly varied set of contributions, quite well anchored around the themes of the Nielsons' work. . The overall quality is excellent. The variety of topics touched is quite broad . ." (Jacques Carette, Computing Reviews, April, 2016)
More details
Other editions
Additional editions
Christian W. Probst | Chris Hankin | René Rydhof Hansen
Semantics, Logics, and Calculi
Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays
Book
12/2015
Springer
€53.49
Shipment within 10-15 days
Content
- Intro
- Preface
- Contents
- Effect Systems Revisited---Control-Flow Algebra and Semantics
- 1 Introduction and Musical Homily
- 1.1 Effect Systems for Music
- 1.2 Section Conclusion and Placement
- 2 Monads and Effect Systems
- 2.1 Traditional Effects
- 2.2 Effects and Monads---Syntactically
- 2.3 Effects and Monads---Weakly Semantically
- 2.4 Effects and Monads---Strongly Semantically via Gradedness
- 2.5 Type-Directed and Effect-Directed Analysis and Semantics
- 3 Control-Flow Effects and Monad Limitations
- 3.1 (Graded) Monadic Semantics for Conditionals
- 3.2 Effect Operators for Conditional
- 3.3 Control-Flow Operators
- 4 Joinads and Rich Effect Systems for Control Flow
- 4.1 Joinads and Conditional Joinads
- 4.2 Type-Directed Semantics Using Conditional Joinads
- 4.3 Classical Joinads
- 4.4 Control-Flow Algebras and Graded Joinads
- 4.5 Classical Joinads---Grading and Control-Flow Algebra
- 5 Discussion
- A Issues Surrounding Monadic Strength
- References
- Last Mile's Resources
- 1 Introduction
- 2 An Example
- 3 MLCoDa with Resources
- 4 Types
- 4.1 History Expressions
- 4.2 Types and Effects
- 5 Loading Time Analysis
- 6 Conclusions
- References
- Formal Modelling and Analysis of Socio-Technical Systems
- 1 Introduction
- 2 The Drama of the Birthday Cake in Three Pictures
- 3 Modelling Socio-Technical Systems
- 3.1 Semantics of Socio-Technical Models
- 3.2 The Bakery Model
- 4 Flow Logic-Based Analysis of Processes
- 4.1 Analysing the Bakery Example
- 5 Attack Generation
- 5.1 Post-Processing Attack Trees
- 5.2 Attack Tree for the Bakery Example
- 6 Analysis of Socio-Technical Attacks in Isabelle
- 6.1 Social Explanation for Insider Threats in Isabelle
- 6.2 Attack Trees in Isabelle
- 7 Related Work
- 8 Conclusion
- References
- Static Timing Analysis -- What is Special?
- 1 Introduction
- 1.1 Timing Analysis
- 1.2 What is Different?
- 2 From Microarchitectures to Abstractions for Timing Analysis
- 2.1 Analysis Framework
- 2.2 Separation into Value and Microarchitectural Analysis
- 2.3 Microarchitectural Analysis
- 2.4 Two Abstractions for Caches
- 3 An Abstractable Pipeline
- 4 Conclusions
- References
- An Automata-Based Approach to Trace Partitioned Abstract Interpretation
- 1 Introduction
- 2 Related Work
- 3 Abstract Interpretation and Trace Partitioning
- 4 Lattice Automata
- 5 Abstract Interpretation as Lattice Model Checking
- 5.1 Final Control Location Partitioning
- 5.2 Control Flow Based Partitioning
- 5.3 Value Based Partitioning
- 5.4 Dynamic Partitioning
- 6 Experiments
- 7 Conclusion
- References
- Probabilistic Abstract Interpretation: From Trace Semantics to DTMC's and Linear Regression
- 1 Introduction
- 2 Probabilistic Semantics
- 2.1 A Probabilistic Language
- 2.2 Kozen's Fixed-Point Semantics (KFS)
- 2.3 Linear Operator Semantics (LOS)
- 2.4 Maximal Trace Semantics (MTS)
- 3 Probabilistic Vs Classical Abstract Interpretation
- 4 Comparison of Probabilistic Semantics
- 5 Statistical Analysis of Probabilistic Programs via PAI
- 5.1 The Linear Statistical Model
- 5.2 Application to Security Analysis
- 5.3 Abstraction and Linear Regression
- 6 Conclusions
- References
- Abstract Interpretation of PEPA Models
- 1 Introduction
- 2 Related Work
- 3 Background
- 3.1 PEPA
- 3.2 Concrete Semantics
- 4 Abstract Interpretation of PEPA Models
- 4.1 Overview
- 4.2 Scalable Differential Semantics
- 5 Modelling a Distributed Denial of Service Attack
- 5.1 Model Parameters, for All Models
- 5.2 First Model: Server and Clients only
- 5.3 Second Model: Adding the Attackers
- 5.4 Third Model: Adding the Defenders
- 6 Discussion and Conclusions
- References
- Static Analysis of Parity Games: Alternating Reachability Under Parity
- 1 Introduction
- 2 Background
- 3 Alternating Reachability Under Parity
- 4 Monotone Functions for a Partial Solver
- 5 Fatal Attractors
- 6 Experimental Results
- 7 Other Related Work
- 8 Conclusions
- References
- Game Theory and Industrial Control Systems
- 1 Introduction
- 2 Vulnerabilities
- 3 Controls
- 4 Game Theory and Cyber Security
- 4.1 A Hybrid Approach
- 5 Conclusions
- References
- Playing with Abstraction and Representation
- 1 Introduction and Motivation
- 2 Contribution
- 3 The Essence of Partition Refinement: The What Perspective
- 4 Property-Oriented Expansion
- 5 CEGAR: Automated Partition Refinement
- 5.1 CFG-Based CEGAR
- 5.2 Predicate-Based CEGAR
- 6 Automata Learning, or Black-Box Partition Refinement
- 6.1 Black-Box Checking
- 7 Discussion of the Profiles and Perspectives
- References
- Schedulers are no Prophets
- 1 Introduction
- 2 Preliminaries
- 2.1 Probability Theory
- 2.2 Stochastic Automata
- 2.3 Uncountable Transition Systems
- 2.4 Variables and Expressions
- 3 Prophetic and Divine Scheduling
- 3.1 Residual Lifetimes [10]
- 3.2 Spent Lifetimes [8]
- 4 Non-prophetic Semantics
- 4.1 Definition
- 4.2 Absence of Prophetic and Divine Behaviour
- 5 Towards Non-Prophetic Model Checking
- 5.1 Stochastic Timed Automata [6]
- 5.2 Residual-Lifetimes Embedding of SA
- 5.3 Embedding of SA with Non-prophetic Semantics
- 5.4 Analysis of STA
- 6 Discussion and Conclusion
- References
- Replicating Data for Better Performances in X10
- 1 Introduction
- 2 X10 in a Nutshell
- 3 Experiments
- 4 Conclusions
- A Results for Eight-Places Scenario
- References
- Guards, Failure, and Partiality: Dijkstra's Guarded-Command Language Formulated Topologically
- 1 Review: The Guarded-Command Language
- 1.1 GCL's Model Theory
- 1.2 What This Paper Accomplishes
- 2 Technical Background
- 2.1 Domains
- 2.2 Scott Topology
- 2.3 General Topology
- 2.4 Powerdomains
- 2.5 Powerspace Topologies and Multifunctions
- 3 Properties of [ ] and "426830A "526930B
- 4 Predicate Transformers
- 4.1 Predicate Transformers are Inverse-Image Maps
- 4.2 Predicate Transformers for the Powerdomains
- 5 Execution Semantics of GCL
- 5.1 Failure and Divergence
- 6 Correctness of Dijkstra's Laws
- 7 Conclusion
- References
- Enhancing Top-Down Solving with Widening and Narrowing
- 1 Introduction
- 2 Equation System
- 3 Widening and Narrowing
- 4 Enhancing TD
- 5 Proof of Termination
- 6 Conclusion
- References
- Modal Intersection Types, Two-Level Languages, and Staged Synthesis
- 1 Introduction
- 2 Modal -calculus with Intersection Types
- 2.1 System
- 3 Subtyping and Distributivity
- 3.1 Modal Intersection Type Subtyping
- 3.2 Subtyping and -principles
- 4 Two-Level Language
- 4.1 Object Language L1
- 4.2 Metalanguage L2/L1
- 4.3 Logical Considerations
- 5 Application to Staged Composition Synthesis
- 5.1 Staged Composition Synthesis
- 5.2 Example
- 6 Conclusion and Further Work
- References
- Rule Formats for Bounded Nondeterminism in Structural Operational Semantics
- 1 Introduction
- 2 Preliminaries
- 3 Finite Branching
- 4 Initials Finiteness
- 5 Image Finiteness
- 6 Future Work
- References
- Author Index
