As malicious code has become more sophisticated and pervasive, faster and more effective system for forensics and prevention is important. Particularly, quick analysis of polymorphic (partly encrypted) viral code is necessary. In this paper we propose a parallel analysis of polymorphic viral code using automated deduction system. In proposed system, decipher routine and its parameters are detected by parallelized automated theorem proving. We apply the weighting and look-ahead heuristics for parallel analysis. We run several detection programs with different computing strategies for analyzing target viral binary code. When the fastest detection process is finished with computing time