I research static analyses based on abstract interpretation to enable verification of software contracts in distributed programs.