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

DOI10.1007/S10817-018-9457-5zbMATH Open1451.68169OpenAlexW2792757320MaRDI QIDQ1663238FDOQ1663238

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Dafny: An Automatic Program Verifier for Functional Correctness
• TweetNaCl: A Crypto Library in 100 Tweets
• 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
• 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 theory of indirection via approximation

Cited In (10)

• \textsf{LOGIC}: a Coq library for logics
• Abstraction and subsumption in modular verification of C programs
• A solver for arrays with concatenation
• Efficient extensional binary tries
• Trace-Relating Compiler Correctness and Secure Compilation
• Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
• Title not available (Why is that?)
• VST-Floyd
• Abstraction and subsumption in modular verification of C programs
• Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method

Uses Software

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

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)