Research is proposed on the specification and verification of computer programs written in languages that provide a low-level view of storage and other resources. This research will focus on novel formal methods for two particularly crucial programming techniques:Shared mutable data structure - the use of representations that may contain more than one pointer to a location that can be updated by the program. These data representations will be specified in an extension of predicate logic, called separation logic, in which the structure of assertions mirrors the separation of storage into Disjoint components. Embedded code pointers - the use of data representations Containing updatable components that point to program instructions. Programs using code pointers will be specified by using a reflection Operator that allows code to occur within assertions.
Specific aspects of low-level programming to be investigated include storage allocation, share-variable concurrency, and the relation between specifications and tye systems. As a consequence of this research, it will become easier to avoid errors in an important class of useful but difficult computer programs. Eventually, it should be possible to automate the logic so that programs in this Class can be accompanied by machine-checkable proofs of their correctness
