Model checking software with symbolic trajectory evaluation

Abstract

Traditional methods of testing computer systems, although valuable, are inadequate for ensuring sufficiently high quality in systems in which a high degree of reliability must be placed. Formal methods for development of hardware and software offer considerable promise in improving quality. Symbolic methods for model checking (e.g. [13]) have had considerable success in the verification of hardware, and a number of industrial concerns use such methods in their design process. The verification of software is much more difficult. Automatic model checking is attractive because it is automatic, but the computational cost may be prohibitive, motivating research with the ultimate goal of finding (relatively) automated, tractable methods of verifying software. Symbolic trajectory evaluation (STE) may be a good starting point since it is able to deal with very large state spaces. This paper presents the first step in the research project of extending the theory of STE to a framework suitable for verifying software.