Semantics, Logics, and Calculi

Name: Semantics, Logics, and Calculi | Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays

Christian W. Probst Chris Hankin René Rydhof Hansen(Herausgeber*in)

Springer (Verlag)

Erschienen am 7. Januar 2016

X, 345 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-27810-0 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken

Semantics, Logics, and Calculi

Beschreibung

Rezensionen / Stimmen

Weitere Details

Weitere Ausgaben

Inhalt

Systemvoraussetzungen