VST-Floyd: a separation logic tool to verify correctness of C programs
type: Item
instance of: scholarly article
title: VST-Floyd: a separation logic tool to verify correctness of C programs
zbMATH Open document ID: 1451.68169
author: Qinxiang Cao
author: Lennart Beringer
author: Samuel Gruetter
author: Josiah Dodds
author: Andrew W. Appel
published in: Journal of Automated Reasoning
publication date: 2018-08-21T00:00:00Z
full work available at URL: https://hdl.handle.net/1721.1/131755
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 6921419
zbMATH Keywords: separation logic
zbMATH Keywords: symbolic execution
zbMATH Keywords: program verification
zbMATH Keywords: proof automation
describes a project that uses: Coq
describes a project that uses: TweetNaCl
describes a project that uses: Dafny
describes a project that uses: Toolchain
describes a project that uses: CBMC
describes a project that uses: HIP
describes a project that uses: Charge!
describes a project that uses: Bedrock
MaRDI profile type: Publication
OpenAlex ID: W2792757320
cites work: Program Logics for Certified Compilers
cites work: Charge!
cites work: Programming Languages and Systems
cites work: TweetNaCl: A Crypto Library in 100 Tweets
cites work: Compositional shape analysis by means of bi-abduction
cites work: Automated verification of shape, size and bag properties via user-defined predicates in separation logic
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Q5584402
cites work: Verified Characteristic Formulae for CakeML
cites work: An axiomatic basis for computer programming
cites work: A theory of indirection via approximation
cites work: The ramifications of sharing in data structures
cites work: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
cites work: The Essence of Higher-Order Concurrent Separation Logic
cites work: Interactive proofs in higher-order concurrent separation logic
cites work: Dafny: An Automatic Program Verifier for Functional Correctness
cites work: Verification Condition Generation Via Theorem Proving
cites work: Q4411818
DOI: 10.1007/S10817-018-9457-5
description: scientific article; zbMATH DE number 6921419