Termination Analysis for the \$\pi\$-Calculus by Reduction to Sequential Program Termination
summary
Proposes an automated reduction that translates π-calculus to C so termination of the sequential program implies termination of the original process, and augments the basic translation with CHC-driven refinement channel types to recover value constraints from non-replicated inputs. Implements a tool that uses Spacer/Z3 and HoIce for CHC solving and Ultimate Automizer for C termination checking. Tests show the refined method verifies many cases TyPiCal cannot, but it fails on four benchmarks due to cross-channel synchronization limits.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:30Outline
- 1:44TT-Calculus
- 5:42Weakness of Basic Translation
- 6:59Our Solution
- 8:21Refinement Type Inference via CHC solving
- 9:32Pitfall in Refinement Type Inference
- 10:41Implementation
- 11:20Experiments
- 12:53Related Work
- 13:38Conclusion
related talks
28mA Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in
21mMechanizing the CMP Abstraction for Parameterized Verification
25mProperty-agnostic base case extension for scalable verification of distributed systems
15mProducts of Recursive Programs for Hypersafety Verification
28mReasoning about Distributed Reconfigurable Systems
13mCharacterizing Implementability of Global Protocols with Infinite States and Data
25mRelax! The Semilenient Core of Choreographic Programming (Functional Pearl)
29mRewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata