IP3 2018-Computer Security 2

This patent is generally related to program security. Disclosed are techniques to ensure maximum security in verifying safety properties of byte code programs translated from Java code. These techniques map byte code functions and interpreter state space into finite states, enter type information to check byte code acceptability, determine properties of acceptable byte code, enter into model checker, interpret each individual condition, verify whether conditions are fulfilled and release byte code for further processing. The technology may be implemented in program testing software, interpreters, java virtual machines, etc.