Static Verification of Worm and virus Behavior in binary Executables using Model Checking