VST-Floyd: a separation logic tool to verify correctness of C programs

DOI10.1007/S10817-018-9457-5MaRDI QIDQ1663238zbMATH OpenOpenAlexFDO

Authors Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel

Publication date 21 August 2018

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://hdl.handle.net/1721.1/131755

zbMATH Keywords

program verificationseparation logicproof automationsymbolic execution

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Program logics for certified compilers
• Computer Science Logic
• Verified heap theorem prover by paramodulation
• Abstraction and subsumption in modular verification of C programs
• C-language floating-point proofs layered with VST and Flocq

Cites work

• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• A theory of indirection via approximation
• An axiomatic basis for computer programming
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Charge! A framework for higher-order separation logic in Coq
• Compositional shape analysis by means of bi-abduction
• Dafny: an automatic program verifier for functional correctness
• Interactive proofs in higher-order concurrent separation logic
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Program logics for certified compilers
• Programming Languages and Systems
• The essence of higher-order concurrent separation logic
• The ramifications of sharing in data structures
• Tools and Algorithms for the Construction and Analysis of Systems
• TweetNaCl: A Crypto Library in 100 Tweets
• Verification Condition Generation Via Theorem Proving
• Verified characteristic formulae for CakeML

Cited in

(18)

• \textsf{LOGIC}: a Coq library for logics
• Mostly sound type system improves a foundational program verifier
• HOL-Boogie -- an interactive prover-backend for the verifying C compiler
• Abstraction and subsumption in modular verification of C programs
• A solver for arrays with concatenation
• Efficient extensional binary tries
• Verified heap theorem prover by paramodulation
• Program logics for certified compilers
• Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
• Separation logic-based verification atop a binary-compatible filesystem model
• VST-Floyd
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Verified software toolchain (invited talk)
• Semi-automated reasoning about non-determinism in C expressions
• Abstraction and subsumption in modular verification of C programs
• Trace-relating compiler correctness and secure compilation
• Featherweight VeriFast
• Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method

Describes a project that uses

Uses Software

• Bedrock
• Charge!
• TweetNaCl
• HIP
• CBMC
• Toolchain
• Dafny
• Coq

This page was built for publication: VST-Floyd: a separation logic tool to verify correctness of C programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663238)