A Static Analysis for Beta-Binders

We introduce a Control Flow Analysis, that statically approximates the dynamic behaviour of processes, expressed in the Beta-Binders calculus. Our analysis of a system is able to describe the essential behaviour of each box, tracking all the possible bindings of variables and all the possible intra- e inter-boxes communications. The analysis offers a basis for establishing static checks of biological dynamic properties. We finally apply our analysis to an example, based on an abstract specification of the interaction between a virus and cells of the immune system.