A local approach for temporal model checking of Java bytecode

Modern computing applications require highly reliable software systems, but current validation techniques, like testing, fail to assure an adequate level of correctness. We present a model checking procedure to verify a subset of the Java virtual machine language (JVML) with respect to properties expressed by a temporal logic. A tableau-based method is developed to prove the satisfaction of a formula: by this local approach a program computation is checked only if involved in the goal of the property verification. A special symbol ⊥ is introduced to represent “unknown'' values, and computations are performed in a symbolic way exploiting the set of guards present in the formulae to refine possible unknown values. This kind of abstraction cuts the state explosion of the programs and it is applicable to check arbitrary formulae, but the result of the verification has an imprecision degree depending on the number of unknown values manipulated during each symbolic computation.