The short version is similar to the one that appears in the proceedings
[
pdf].
The long version provides definitions, examples and proofs [
pdf].
An implementation in Ocaml of the algorithm that computes buffer bounds can be found here [
ml].
The slides from the CONCUR presentation in Paris.
[
pdf].