Smallfoot
From MaRDI portal
Software:21766
No author found.
Related Items (53)
Formal verification of parallel prefix sum and stream compaction algorithms in CUDA ⋮ Completeness for recursive procedures in separation logic ⋮ A First-Order Logic with Frames ⋮ Crowfoot: A Verifier for Higher-Order Store Programs ⋮ Symbolic execution proofs for higher order store programs ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ Certifying low-level programs with hardware interrupts and preemptive threads ⋮ Caper ⋮ Automated Theorem Proving for Assertions in Separation Logic with All Connectives ⋮ Completeness for a First-Order Abstract Separation Logic ⋮ Practical Tactics for Separation Logic ⋮ A Formalisation of Smallfoot in HOL ⋮ Shape Neutral Analysis of Graph-based Data-structures ⋮ Featherweight VeriFast ⋮ Effective interactive proofs for higher-order imperative programs ⋮ Separation logic with one quantified variable ⋮ Specification patterns for reasoning about recursion through the store ⋮ Separation logics and modalities: a survey ⋮ Proof tactics for assertions in separation logic ⋮ Compositional entailment checking for a fragment of separation logic ⋮ Disjoint-union partial algebras ⋮ Reasoning about memory layouts ⋮ Reasoning about sequences of memory states ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Temporary Read-Only Permissions for Separation Logic ⋮ Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ⋮ Lightweight Separation ⋮ Static Analysis ⋮ Reasoning about Assignments in Recursive Data Structures ⋮ Compositional Shape Analysis by Means of Bi-Abduction ⋮ A proof system for separation logic with magic wand ⋮ Decision procedures. An algorithmic point of view ⋮ Verified heap theorem prover by paramodulation ⋮ Proof automation for functional correctness in separation logic ⋮ Verification of Concurrent Systems with VerCors ⋮ Viper: A Verification Infrastructure for Permission-Based Reasoning ⋮ Automated Verification of Shape and Size Properties Via Separation Logic ⋮ Automatic Parallelization with Separation Logic ⋮ A Basis for Verifying Multi-threaded Programs ⋮ Beyond Shapes: Lists with Ordered Data ⋮ Verifying Reference Counting Implementations ⋮ Unifying separation logic and region logic to allow interoperability ⋮ A shape graph logic and a shape system ⋮ On Temporal and Separation Logics ⋮ Juggrnaut: using graph grammars for abstracting unbounded heap structures ⋮ Specification Patterns and Proofs for Recursion through the Store ⋮ Tractable Reasoning in a Fragment of Separation Logic ⋮ Automatic Parallelization and Optimization of Programs by Proof Rewriting ⋮ Tableaux and Resource Graphs for Separation Logic ⋮ Separation Logic Tutorial ⋮ Matching Logic ⋮ Local Reasoning about Data Update ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
This page was built for software: Smallfoot
