Analysis of Source Code: A Case Study
Danita Hartley and Padmanabhan Krishnan
Department of Computer Science
University of Canterbury
Abstract
This paper summarises our experience in using model checking technology to understand concurrent programs. We use Verisoft to understand various aspects of a firewall tool kit. The main conclusion is that it is possible to inspect source code with a view towards verifying key behavioural properties.