## User login## Navigation |
## Process algebra needs proof methodologyIt's widely appreciated that knowing that a distributed system or protocol behaves correctly is generally hard, and that process algebras provide useful formalisms for reasoning about these. Less appreciated is how hard it is to turn informal correctness proofs into formal proofs using process algebras. Process algebra needs proof methodology (Fokkink, Groote & Reniers), an introductory article published a year ago in the Bulletin of the EATCS, provides a nice introduction to the problem of making process algebras more tractable for correctness reasoning, using Tanenbaum's sliding window protocol as a running example of a surprisingly hard-to-formalise proof. Perhaps as interesting for LtU readers is that the article comes from the negelected "third" approach to process algebra (after CCS and CSP), namely the Algebra of Communicating Processes of Bergstra and Klop. |
## Browse archives## Active forum topics |

## Recent comments

7 hours 47 min ago

1 day 7 hours ago

1 day 9 hours ago

1 day 9 hours ago

2 days 15 hours ago

2 days 16 hours ago

3 days 10 hours ago

3 days 12 hours ago

3 days 12 hours ago

4 days 4 hours ago