Program Analysis

A broad research field which addresses the general concern of software safety is program analysis (from now on PA for short), in which we ensure/detect programs' significant properties by analysing their source code. The field started from the classical methods such as data/control flow analyses [56], received enrichment from semantic studies in the form of abstract interpretation [56], gained new impetus and methods from software model checking [19], and, more recently, incorporated diverse type-based analyses [57] where type-information is used crucially for the analyses (often using variants of type and effect disciplines [8]). Program analysis is a rich field, and is being rapidly applied to practice. The following prominent national/international initiatives (in both academia and industry) give a partial list of activities which witness the significance of PA in today's software technologies.

1. The EU-sponsored projects, including SecSafe [64] and VerifiCard [66], which studied diverse PA techniques for verifying safety of Javacard (a subset of Java for smart-cards), involving several European universities and industry partners.

2. The ESC/Java project (ESC stands for ``extended static checker'') [30] at Compac Systems Research Center. This project constructs a comprehensive set of static and semi-static PA tools for the sequential part of Java.

3. The SLAM project at Microsoft Research (Redmond) [9]. This project develops a static checker of certain temporal properties of sequential C programs, using model checking techniques. The tool is currently being used for checking basic safety properties of real OS drivers.

These and other works indicate broad and strong interests in mathematically-based methods for safety of software, as well as the maturing of the technologies which would enable these methods. As indicated by the descriptions above, many projects explicitly rely on well-studied semantic and logical frameworks established through long-running investigation in the Theoretical Computer Science community.