VST-Floyd: a separation logic tool to verify correctness of C programs
From MaRDI portal
Publication:1663238
DOI10.1007/s10817-018-9457-5zbMath1451.68169OpenAlexW2792757320MaRDI QIDQ1663238
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
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (8)
Trace-Relating Compiler Correctness and Secure Compilation ⋮ Abstraction and subsumption in modular verification of C programs ⋮ Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method ⋮ A solver for arrays with concatenation ⋮ Efficient extensional binary tries ⋮ \textsf{LOGIC}: a Coq library for logics ⋮ Unnamed Item ⋮ VST-Floyd
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Iris
- Charge!
- The ramifications of sharing in data structures
- TweetNaCl: A Crypto Library in 100 Tweets
- Verified Characteristic Formulae for CakeML
- The Essence of Higher-Order Concurrent Separation Logic
- Dafny: An Automatic Program Verifier for Functional Correctness
- A theory of indirection via approximation
- Compositional shape analysis by means of bi-abduction
- Tools and Algorithms for the Construction and Analysis of Systems
- Interactive proofs in higher-order concurrent separation logic
- Verification Condition Generation Via Theorem Proving
- Programming Languages and Systems
- Program Logics for Certified Compilers
- An axiomatic basis for computer programming
This page was built for publication: VST-Floyd: a separation logic tool to verify correctness of C programs
