Verifying temporal specifications of Java programs