Checking program proofs made easy

To generate reliable software, it must be shown that a program meets its specifications. This can be done using program verification techniques. Assertions are made about the expected behavior of a program, and intermediate program states are examined to ensure that the program specifications are never violated. However,proving that the intermediate program steps lead to the conclusion and, therefore, proving that the program is correct is difficult. In this paper we introduce a novel technique, temporal subsumption, and its application as a proof checker. This technique removes “redundant” assertions from an argument of program correctness, based on a precondition and the predicate transformations performed by the program statements