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

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

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.