Reasoning About Low-Level Programming

点击翻译按钮获取中文摘要

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 intoDisjoint components. Embedded code pointers - the use of data representationsContaining updatable components that point to program instructions. Programs using code pointers will be specified by using a reflectionOperator that allows code to occur within assertions.Specific aspects of low-level programming to be investigated includestorage allocation, share-variable concurrency, and the relationbetween specifications and tye systems.As a consequence of this research, it will become easier to avoiderrors in an important class of useful but difficult computer programs. Eventually, it should be possible to automate the logic so that programs in thisClass can be accompanied by machine-checkable proofs of their correctness