VeriFast: Semi-Automated Modular Verification of Concurrent C and Java Programs Using Separation Logic