The following pages link to Smallfoot (Q21766):
Displaying 50 items.
- Completeness for recursive procedures in separation logic (Q278747) (← links)
- Symbolic execution proofs for higher order store programs (Q287265) (← links)
- Specification patterns for reasoning about recursion through the store (Q393092) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- Decision procedures. An algorithmic point of view (Q518892) (← links)
- Reasoning about memory layouts (Q633298) (← links)
- Reasoning about sequences of memory states (Q636268) (← links)
- A shape graph logic and a shape system (Q744329) (← links)
- Juggrnaut: using graph grammars for abstracting unbounded heap structures (Q746781) (← links)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms (Q832310) (← links)
- Certifying low-level programs with hardware interrupts and preemptive threads (Q835764) (← links)
- Proof tactics for assertions in separation logic (Q1687747) (← links)
- Compositional entailment checking for a fragment of separation logic (Q1688543) (← links)
- Unifying separation logic and region logic to allow interoperability (Q1798668) (← links)
- Formal verification of parallel prefix sum and stream compaction algorithms in CUDA (Q2120963) (← links)
- Separation logic with one quantified variable (Q2411038) (← links)
- Viper: A Verification Infrastructure for Permission-Based Reasoning (Q2796035) (← links)
- Local Reasoning about Data Update (Q2864149) (← links)
- Crowfoot: A Verifier for Higher-Order Store Programs (Q2891407) (← links)
- Effective interactive proofs for higher-order imperative programs (Q2936804) (← links)
- Temporary Read-Only Permissions for Separation Logic (Q2988642) (← links)
- Caper (Q2988651) (← links)
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic (Q2988661) (← links)
- Reasoning about Assignments in Recursive Data Structures (Q2999318) (← links)
- Specification Patterns and Proofs for Recursion through the Store (Q3088293) (← links)
- Tractable Reasoning in a Fragment of Separation Logic (Q3090833) (← links)
- Completeness for a First-Order Abstract Separation Logic (Q3179309) (← links)
- Practical Tactics for Separation Logic (Q3183539) (← links)
- A Formalisation of Smallfoot in HOL (Q3183546) (← links)
- Featherweight VeriFast (Q3196351) (← links)
- Automatic Parallelization and Optimization of Programs by Proof Rewriting (Q3392920) (← links)
- Tableaux and Resource Graphs for Separation Logic (Q3406689) (← links)
- Automated Theorem Proving for Assertions in Separation Logic with All Connectives (Q3454118) (← links)
- Lightweight Separation (Q3543659) (← links)
- Automatic Parallelization with Separation Logic (Q3617713) (← links)
- A Basis for Verifying Multi-threaded Programs (Q3617715) (← links)
- Beyond Shapes: Lists with Ordered Data (Q3617745) (← links)
- Verifying Reference Counting Implementations (Q3617768) (← links)
- Shape Neutral Analysis of Graph-based Data-structures (Q4559807) (← links)
- Separation logics and modalities: a survey (Q4586138) (← links)
- Matching Logic (Q4600770) (← links)
- A First-Order Logic with Frames (Q5041109) (← links)
- On Temporal and Separation Logics (Q5079764) (← links)
- Verified heap theorem prover by paramodulation (Q5168877) (← links)
- Verification of Concurrent Systems with VerCors (Q5175776) (← links)
- Disjoint-union partial algebras (Q5278076) (← links)
- Compositional Shape Analysis by Means of Bi-Abduction (Q5395670) (← links)
- A proof system for separation logic with magic wand (Q5408443) (← links)
- Automated Verification of Shape and Size Properties Via Separation Logic (Q5452612) (← links)
- Static Analysis (Q5466564) (← links)
