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

被引：11

作者：

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 条

[1]

APPEL AW, 2011, P 20 EUR C PROGR LAN

[2]

Berdine J, 2006, LECT NOTES COMPUT SC, V4111, P115

[3]

Brady Edwin., 2016, TYPE DRIVEN DEV IDRI

[4]

Brotherston J., 2012, LECT NOTES COMPUT SC, P350, DOI 10.1007/978-3-642-35182-2_25

[5]

Chargueraud A, 2011, ICFP 11 - PROCEEDINGS OF THE 2011 ACM SIGPLAN: INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, P418

[6]

Chlipala Adam, 2011, MOSTLY AUTOMATED VER, DOI [10.1145/1993498.1993526, DOI 10.1145/1993498.1993526]

[7] Z3: An efficient SMT solver [J].

de Moura, Leonardo ;

Bjorner, Nikolaj .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 :337-340

[8] A metaprogramming framework for formal verification [J].

Ebner G. ;

Ullrich S. ;

Roesch J. ;

Avigad J. ;

De Moura L. .

1600, Association for Computing Machinery (01)

[9]

FAGES F, 1984, LECT NOTES COMPUT SC, V170, P194

[10]

Garg, PROGRAMMING LANGUAGE

← 1 2 3 4 →