Will focus on the tool support for b-APIs. WP4 will turn the algorithms and the verification, validation, and reverse-engineering techniques identified in WP2 and WP3 into provably correct tool chains