Natarajan Shankar (auth.), Catuscia Palamidessi (eds.)3540678972, 9783540678977
Table of contents :
Combining Theorem Proving and Model Checking through Symbolic Analysis….Pages 1-16
Verification Is Experimentation!….Pages 17-24
Compositional Performance Analysis Using Probabilistic I/O Automata….Pages 25-28
Formal Models for Communication-Based Design….Pages 29-47
Programming Access Control: The K laim Experience….Pages 48-65
Exploiting Hierarchical Structure for Efficient Formal Verification….Pages 66-68
From Process Calculi to Process Frameworks….Pages 69-88
Verification Using Tabled Logic Programming….Pages 89-91
Open Systems in Reactive Environments: Control and Synthesis….Pages 92-107
Model Checking with Finite Complete Prefixes Is PSPACE-Complete….Pages 108-122
Verifying Quantitative Properties of Continuous Probabilistic Timed Automata….Pages 123-137
The Impressive Power of Stopwatches….Pages 138-152
Optimizing Büchi Automata….Pages 153-168
Generalized Model Checking: Reasoning about Partial State Spaces….Pages 168-182
Reachability Analysis for Some Models of Infinite-State Transition Systems….Pages 183-198
Process Spaces….Pages 199-213
Failure Semantics for the Exchange of Information in Multi-Agent Systems….Pages 214-228
Proof-Outlines for Threads in Java….Pages 229-242
Deriving Bisimulation Congruences for Reactive Systems….Pages 243-258
Bisimilarity Congruences for Open Terms and Term Graphs via Tile Logic….Pages 259-274
Process Languages for Rooted Eager Bisimulation….Pages 275-289
Action Contraction….Pages 290-305
A Theory of Testing for Markovian Processes….Pages 305-319
Reasoning about Probabilistic Lossy Channel Systems….Pages 320-333
Weak Bisimulation for Probabilistic Systems….Pages 334-349
Nondeterminism and Probabilistic Choice: Obeying the Laws….Pages 350-365
Secrecy and Group Creation….Pages 365-379
On the Reachability Problem in Cryptographic Protocols….Pages 380-394
Secure Information Flow for Concurrent Processes….Pages 395-409
LP Deadlock Checking Using Partial Order Dependencies….Pages 410-425
Pomsets for Local Trace Languages….Pages 426-441
Functional Concurrent Semantics for Petri Nets with Read and Inhibitor Arcs….Pages 442-457
The Control of Synchronous Systems….Pages 458-473
Typing Non-uniform Concurrent Objects….Pages 474-489
An Implicitly-Typed Deadlock-Free Process Calculus….Pages 489-504
Typed Mobile Objects….Pages 504-520
Synthesizing Distributed Finite-State Systems from MSCs….Pages 521-535
Emptiness Is Decidable for Asynchronous Cellular Machines….Pages 536-551
Revisiting Safety and Liveness in the Context of Failures….Pages 552-565
Well-Abstracted Transition Systems….Pages 566-581
A Unifying Approach to Data-Independence….Pages 581-596
Chi Calculus with Mismatch….Pages 596-610
Reviews
There are no reviews yet.