CROSSBOW demo clusters formal analysis

Summary
Detailed analysis of the CROSSBOW HLUs and demo clusters. Deliverable linked to T2.3