Table of Contents
|
Formal Techniques for Distributed Objects, Components, and Systems
Susanne Graf, Mahesh Viswanathan |
Front Matter |
Ensuring Properties of Distributed Systems
|
Types for Deadlock-Free Higher-Order Programs
Luca Padovani, Luca Novara |
3-18 |
On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency
Alex Horn, Daniel Kroening |
19-34 |
A Strategy for Automatic Verification of Stabilization of Distributed Algorithms
Ritwika Ghosh, Sayan Mitra |
35-49 |
Faster Linearizability Checking via P-Compositionality
Alex Horn, Daniel Kroening |
50-65 |
Translation Validation for Synchronous Data-Flow Specification in the SIGNAL Compiler
Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier |
66-80 |
Formal Models of Concurrent and Distributed Systems
|
Dynamic Causality in Event Structures
Youssef Arbach, David Karcher, Kirstin Peters, Uwe Nestmann |
83-97 |
Loop Freedom in AODVv2
Kedar Namjoshi, Richard Trefler |
98-112 |
Code Mobility Meets Self-organisation: A Higher-Order Calculus of Computational Fields
Ferruccio Damiani, Mirko Viroli, Danilo Pianini, Jacob Beal |
113-128 |
Real Time Systems
|
Timely Dataflow: A Model
Martín Abadi, Michael Isard |
131-145 |
Difference Bound Constraint Abstraction for Timed Automata Reachability Checking
Weifeng Wang, Li Jiao |
146-160 |
Compliance and Subtyping in Timed Session Types
Massimo Bartoletti, Tiziana Cimoli, Maurizio Murgia, Alessandro Podda, Livio Pompianu |
161-177 |
Security
|
Type Checking Privacy Policies in the π-calculus
Dimitrios Kouzapas, Anna Philippou |
181-195 |
Extending Testing Automata to All LTL
Ala Salem |
196-210 |
Efficient Verification Techniques
|
Simple Isolation for an Actor Abstract Machine
Benoit Claudel, Quentin Sabah, Jean-Bernard Stefani |
213-227 |
Sliced Path Prefixes: An Effective Method to Enable Refinement Selection
Dirk Beyer, Stefan Löwe, Philipp Wendler |
228-243 |
