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
• Automated theorem proving for assertions in separation logic with all connectives
• Verifying Reference Counting Implementations
• Automatic Parallelization with Separation Logic
• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
• Separation logics and modalities: a survey
• Completeness for recursive procedures in separation logic
• Shape neutral analysis of graph-based data-structures
• 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
• Symbolic execution proofs for higher order store programs
• A Basis for Verifying Multi-threaded Programs
• Viper: a verification infrastructure for permission-based reasoning
• Matching logic
• 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
• On temporal and separation logics
• Reasoning about assignments in recursive data structures
• A shape graph logic and a shape system
• Certifying low-level programs with hardware interrupts and preemptive threads
• Specification patterns and proofs for recursion through the store
• Tableaux and resource graphs for separation logic
• Temporary read-only permissions for separation logic
• Unifying separation logic and region logic to allow interoperability
• Static Analysis
• Reasoning about memory layouts
• Juggrnaut: using graph grammars for abstracting unbounded heap 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
• Completeness for a first-order abstract separation logic
• Featherweight VeriFast
• A first-order logic with frames
• Beyond Shapes: Lists with Ordered Data
• Crowfoot: A Verifier for Higher-Order Store Programs
• Effective interactive proofs for higher-order imperative programs
• A Formalisation of Smallfoot in HOL
• Local reasoning about data update
• Verification of concurrent systems with VerCors
• Caper
• Decision procedures. An algorithmic point of view
• Compositional shape analysis by means of bi-abduction
• Unified reasoning about robustness properties of symbolic-heap separation logic

This page was built for software: Smallfoot