Reasoning About Low-Level Programming

关于低级编程的推理

• 批准号: 0204242
• 负责人: John Reynolds
• 金额: $ 30万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-09-01 至 2005-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0204242&HistoricalAwards=false
• 关键词: 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

建议研究以提供存储和其他资源的低级视图的语言编写的计算机程序的规范和验证。 这项研究将重点关注两种特别重要的编程技术的新型形式方法：共享可变数据结构——使用可能包含多个指向可由程序更新的位置的指针的表示。这些数据表示将在谓词逻辑的扩展（称为分离逻辑）中指定，其中断言的结构反映了存储到不相交组件的分离。嵌入式代码指针 - 使用数据表示包含指向程序指令的可更新组件。使用代码指针的程序将通过使用允许代码在断言内发生的反射操作符来指定。要研究的低级编程的具体方面包括存储分配、共享变量并发性以及规范和类型系统之间的关系。研究表明，避免一类重要的有用但困难的计算机程序中的错误将变得更加容易。最终，应该可以实现逻辑自动化，以便此类中的程序可以附有机器可检查的正确性证明