Automatic verification of programs: algorithm ALICE

This paper aims to introduce a method for verification of programs, which is fully automatic. This method consists in an algorithm called ALICE which, given a program and an algebraic specification, answers if the program is correct w.r.t. the algebraic specification. No user intervention is needed (except, of course, the writing of the program and the specification). The paper also proves that the problem of determining the correctness of a program w.r.t. an algebraic specification is undecidable (even if only partial correctness is required).Postprint (published version