Browse Prior Art Database

A Method and System for Guiding a Testing Process Using Results of a Failed Verification of Likely Invariants

IP.com Disclosure Number: IPCOM000236340D
Publication Date: 2014-Apr-21
Document File: 2 page(s) / 34K

Publishing Venue

The IP.com Prior Art Database

Abstract

A method and system is disclosed of guiding a testing process using results of a failed verification of likely invariants.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 52% of the total text.

Page 01 of 2

A Method and System for Guiding a Testing Process Using Results of a Failed Verification of Likely Invariants

Verification of complex software systems is a notoriously hard problem . In fact, in some cases the problem of verification is not even decidable . Accordingly, there have been continual efforts to find solutions that enable inferring and proving useful properties of software systems while transcending the transitional limitations of static analysis .

One such solution is to derive likely invariants from dynamic runs of a program . The solution is based on running the program multiple times , and applying templates of likely invariants to the different runs. If a template matches all runs, then the template becomes a candidate for verification, and is identified as a likely invariant. For example, the template can be identified as a match during a particular program point such as, but not limited to, a loop test. Candidate templates identified as likely invariants are then submitted to a prover. The prover either succeeds in proving that the likely invariant is in fact an invariant, or fails in proving that the likely invariant is an invariant. The prover succeeds if it can be proved that the likely invariant does not only hold over some finite number of runs, but in fact holds over all inputs and all runs of the program. Similarly the prover fails if a case wherein the likely invariant fails to hold is identified. If the prover fails, then a counter example representing the case is produced and returned.

However, it has been observed that failure by the prover to prove a likely invariant does not necessarily imply that the likely invariant is not an invariant. Due to the un&decidability of static program analysis, there are cases where the prover errs on the conservative side, and is unable to prove an invariant correct. Empirically, however, likely invariants that the prover is unable to prove as such turn out to be wrong . It has also been observed that the trend of likely invariants turning out to be wrong holds for most program runs. Further, this trend is also seen as the cause b...