9708915 This research focuses on applying formal methods to the problem of certification of imported software. Formal systems such as set constraints, Kleene algebra and Kleene algebra with tests, and the modal mu-calculus have been shown to provide potent tools for practical program analysis and verification. It is proposed to develop these systems further with special focus on efficient practical algorithms and to investigate their use as tools for software certification. The goals are (i) to make it easy for a software vendor to construct a certificate to be downloaded along with a compiled object that ensures that certain safety conditions are met; and (ii) to make it easy for a client to check the certificate to verify that the foreign code is safe to run locally. It is hoped that this work will contribute to the elimination of untrustworthy software. ***
