REGRESSION VERIFICATION BY SYSTEM LAV

Abstract

Software verification tools have achieved enormous progress and are becoming practically usable to a broad set of users. Over the last years, regression verification, a special sort of software verification, is also practically considered. In regression verification, similarly as in regression testing, functional correctness of a program is checked by analyzing its equivalence with the program which is assumed to be correct. Of course, regression verification, when applicable, provides much more reliable and deeper conclusions than regression testing. In this paper we briefly describe basic concepts of software verification and show that the verification system LAV can be successfully used for regression verification. Possible applications are in software development (as an alternative to regression testing), but also in education, for automatic evaluation of students’ programs.