Formal Methods for Android Banking Malware Analysis and Detection