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

该奖项是根据2009年《美国复苏和再投资法案》(Public Law 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.