VST-Floyd: a separation logic tool to verify correctness of C programs (Q1663238): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+TweetNaCl
@@ Property / describes a project that uses: TweetNaCl / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Dafny
@@ Property / describes a project that uses: Dafny / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Toolchain
@@ Property / describes a project that uses: Toolchain / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CBMC
@@ Property / describes a project that uses: CBMC / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HIP
@@ Property / describes a project that uses: HIP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Charge!
@@ Property / describes a project that uses: Charge! / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Bedrock
@@ Property / describes a project that uses: Bedrock / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2792757320
@@ Property / OpenAlex ID: W2792757320 / rank @@
+Normal rank
@@ Property / cites work @@
+Program Logics for Certified Compilers
@@ Property / cites work: Program Logics for Certified Compilers / rank @@
+Normal rank
@@ Property / cites work @@
+Charge!
@@ Property / cites work: Charge! / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+TweetNaCl: A Crypto Library in 100 Tweets
@@ Property / cites work: TweetNaCl: A Crypto Library in 100 Tweets / rank @@
+Normal rank
@@ Property / cites work @@
+Compositional shape analysis by means of bi-abduction
+Normal rank
@@ Property / cites work @@
+Automated verification of shape, size and bag properties via user-defined predicates in separation logic
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Q5584402
@@ Property / cites work: Q5584402 / rank @@
+Normal rank
@@ Property / cites work @@
+Verified Characteristic Formulae for CakeML
@@ Property / cites work: Verified Characteristic Formulae for CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+An axiomatic basis for computer programming
@@ Property / cites work: An axiomatic basis for computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+A theory of indirection via approximation
@@ Property / cites work: A theory of indirection via approximation / rank @@
+Normal rank
@@ Property / cites work @@
+The ramifications of sharing in data structures
@@ Property / cites work: The ramifications of sharing in data structures / rank @@
+Normal rank
@@ Property / cites work @@
+Iris
@@ Property / cites work: Iris / rank @@
+Normal rank
@@ Property / cites work @@
+The Essence of Higher-Order Concurrent Separation Logic
+Normal rank
@@ Property / cites work @@
+Interactive proofs in higher-order concurrent separation logic
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+Verification Condition Generation Via Theorem Proving
+Normal rank
@@ Property / cites work @@
+Q4411818
@@ Property / cites work: Q4411818 / rank @@
+Normal rank