A machine-checked soundness proof for an efficient verification condition generator

2010 ◽  
Author(s):  
Frédéric Vogels ◽  
Bart Jacobs ◽  
Frank Piessens
Keyword(s):  
Verification Condition ◽  
Efficient Verification

scholarly journals Steel: proof-oriented programming in a dependently typed concurrent separation logic

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-30
Author(s):  
Aymeric Fromherz ◽  
Aseem Rastogi ◽  
Nikhil Swamy ◽  
Sydney Gibson ◽  
Guido Martínez ◽  
...  
Keyword(s):  
Linked Data ◽  
Separation Logic ◽  
Concurrent Programs ◽  
Interactive Proof ◽  
First Order ◽  
Session Types ◽  
Verification Condition ◽  
New Formulation ◽  
Concurrent Separation Logic ◽  
Efficient Verification

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.

scholarly journals Efficient Verification of Dicke States

2019 ◽  
Vol 12 (4) ◽  
Author(s):  
Ye-Chao Liu ◽  
Xiao-Dong Yu ◽  
Jiangwei Shang ◽  
Huangjun Zhu ◽  
Xiangdong Zhang
Keyword(s):  
Efficient Verification ◽  
Dicke States

scholarly journals Towards efficient verification of population protocols

2021 ◽  
Author(s):  
Michael Blondin ◽  
Javier Esparza ◽  
Stefan Jaax ◽  
Philipp J. Meyer
Keyword(s):  
Linear Constraints ◽  
Computational Power ◽  
High Complexity ◽  
Reachability Problem ◽  
Population Protocols ◽  
Finite State ◽  
State Agents ◽  
Efficient Verification ◽  
Primitive Recursive ◽  
Very High

AbstractPopulation protocols are a well established model of computation by anonymous, identical finite-state agents. A protocol is well-specified if from every initial configuration, all fair executions of the protocol reach a common consensus. The central verification question for population protocols is the well-specification problem: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is -hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class $${ WS}^3$$ WS 3 of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that $${ WS}^3$$ WS 3 has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership and correctness problems for $${ WS}^3$$ WS 3 reduce to solving boolean combinations of linear constraints over $${\mathbb {N}}$$ N . This allowed us to develop the first software able to automatically prove correctness for all of the infinitely many possible inputs.

Sign in / Sign up

Export Citation Format

Share Document