Software Regression Verification
Abstract
The objective of this research effort was to study and develop a formal methodology for conducting automated or semiautomated software regression testing. To that end, we have developed and extended a regression verification tool (RVT) in various ways, which together improved tremendously its functionality, robustness and completeness. Recall that the main problem that RVT addresses is that of deciding whether two similar programs are equivalent under an arbitrary yet equal context, given some definition of equivalence. More precisely, given a (possibly partial) mapping between the functions of the two programs, the problem is to show which of them are equivalent in an arbitrary context. The basic definition of equivalence that we support is called partial equivalence, which means that two programs emit equal outputs given the same inputs, or at least one of them does not terminate. For most useful definitions of equivalence this problem is undecidable, as is the problem of partial correctness (what most people refer to as general program verification) in general.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 11, 2013
- Accession Number
- ADA594501
Entities
People
- Ofer Strichman
Organizations
- Technion – Israel Institute of Technology