SHF: Small: Specification, Verification, and Semantics of Higher-Order and Concurrent Software

该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。为了扩展分离逻辑和无粒度语义的规模和通用性，使其适用于更复杂和更多样化的软件系统的规范和验证，正在进行以下研究计划： 高阶设计模式-使用高阶分离逻辑 在面向对象编程中指定设计模式，并验证其 实施. 高阶程序设计语言的扩展-扩展分离 逻辑转换为具有堆的类似Algol的语言，包括 允许全局信息隐藏。 无颗粒语义-设计一种新形式的无颗粒语义， 对共享变量并发性的更抽象、更简洁的描述， 避免对默认原子性级别的任何承诺。 逻辑和语义的实现-使用Isabelle/HOL系统 实现分离逻辑中证明的机器辅助构造， 一种既能保证证明的有效性，又能保证证明的可靠性的方法。 逻辑及其扩展。总体目标是大大增加可以通过分离逻辑验证的程序的种类，并促进此逻辑和其他共享变量并发逻辑的合理性论证。

This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5).To extend the scale and generality of separation logic and grainless semanticsto become applicable to the specification and verification of more complex andvaried software systems, the following research initiatives are being pursued: Higher-Order Design Patterns - Using higher-order separation logic to specify design patterns in object-oriented programing, and to verify their implementation. Extension to a Higher-Order Programming Language - extending separation logic to an Algol-like language with a heap, including procedures that permit global information hiding. Grainless Semantics - devising a new form of grainless semantics that gives a more abstract and concise description of shared-variable concurrency by avoiding any commitment to a default level of atomicity. Implementation of Logics and Semantics - Using the Isabelle/HOL system to implement the machine-aided construction of proofs in separation logic in a way that ensures both the validity of the proofs and the soundness of the logic and its extensions.The overall goal is to substantially increase the variety of programs that canbe verified by separation logic, and to facilitate soundness arguments for thisand other logics for shared-variable concurrency.