VST-Floyd: a separation logic tool to verify correctness of C programs
DOI10.1007/S10817-018-9457-5zbMATH Open1451.68169OpenAlexW2792757320MaRDI QIDQ1663238FDOQ1663238
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
Recommendations
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)
Cites Work
- Dafny: an automatic program verifier for functional correctness
- TweetNaCl: A Crypto Library in 100 Tweets
- Title not available (Why is that?)
- An axiomatic basis for computer programming
- Programming Languages and Systems
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Compositional shape analysis by means of bi-abduction
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification Condition Generation Via Theorem Proving
- Title not available (Why is that?)
- Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
- Verified characteristic formulae for CakeML
- The essence of higher-order concurrent separation logic
- The ramifications of sharing in data structures
- Interactive proofs in higher-order concurrent separation logic
- Program logics for certified compilers
- Charge! A framework for higher-order separation logic in Coq
- A theory of indirection via approximation
Cited In (18)
- \textsf{LOGIC}: a Coq library for logics
- Mostly sound type system improves a foundational program verifier
- Abstraction and subsumption in modular verification of C programs
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- 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
- Title not available (Why is that?)
- Verified software toolchain (invited talk)
- VST-Floyd
- Semi-automated reasoning about non-determinism in C expressions
- Trace-relating compiler correctness and secure compilation
- Abstraction and subsumption in modular verification of C programs
- Featherweight VeriFast
- Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method
Uses Software
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)
