Automatic software verification based on reverse engineering and deduction: A brief description of the ALICE system

摘要

A fully automatic method for verification of programs and its implementation (named "the ALICE system") are introduced. The method is discussed and the problems that it entails are solved. Furthermore, the paper contains a description of thedifferent parts of the ALICE system as well as of its theoretical foundations.