Smallfoot

swMATH9787MaRDI QIDQ21766FDOQ21766

Author name not available (Why is that?)

Cited In (53)

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

This page was built for software: Smallfoot