Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic

被引：12

作者：

Fromherz, Aymeric ^{[1
]}

Rastogi, Aseem ^{[2
]}

Swamy, Nikhil ^{[3
]}

Gibson, Sydney ^{[1
]}

Martinez, Guido ^{[4
]}

Merigoux, Denis ^{[5
]}

Ramananandro, Tahina ^{[3
]}

机构：

[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA

[2] Microsoft Res, Bengaluru, Karnataka, India

[3] Microsoft Res, Redmond, WA USA

[4] Consejo Nacl Invest Cient & Tecn, CIFASIS, Buenos Aires, DF, Argentina

[5] Inria Paris, Paris, France

来源：

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2021年 / 5卷

基金：

欧洲研究理事会; 美国国家科学基金会;

关键词：

Program Proofs; Separation Logic; Concurrency;

D O I：

10.1145/3473590

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Steel is a language for developing and proving concurrent programs embedded in F*, a dependently typed programming language and proof assistant. Based on SteelCore, a concurrent separation logic (CSL) formalized in F*, our work focuses on exposing the proof rules of the logic in a form that enables programs and proofs to be effectively co-developed. Our main contributions include a new formulation of a Hoare logic of quintuples involving both separation logic and first-order logic, enabling efficient verification condition (VC) generation and proof discharge using a combination of tactics and SMT solving. We relate the VCs produced by our quintuple system to solving a system of associativity-commutativity (AC) unification constraints and develop tactics to (partially) solve these constraints using AC-matching modulo SMT-dischargeable equations. Our system is fully mechanized and implemented in F*. We evaluate it by developing several verified programs and libraries, including various sequential and concurrent linked data structures, proof libraries, and a library for 2-party session types. Our experience leads us to conclude that our system enables a mixture of automated and interactive proof, making it productive to build programs foundationally verified against a highly expressive, state-of-the-art CSL.

引用

页数：30

共 37 条

[21]

MULLER P, 2016, VERIFICATION MODEL C, V9583

[22] Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations [J].