Modular verification of concurrent assembly code with dynamic thread creation and termination