Our Approach
Identify deterministic/deadlock-free partsby a static type system
Enrich Channel Types with Information of
- ¡ÈIn what way a channel is used¡É ? Linear Channels, Usage Annotations
- ¡ÈIn what order channels are used¡É ? Time Tags
Rationale:Type systems are usually compositional & tractable (unlike model checking, abstract interpretation, etc.)