The following pages link to HIP (Q21765):
Displayed 32 items.
- Completeness for recursive procedures in separation logic (Q278747) (← links)
- Symbolic execution proofs for higher order store programs (Q287265) (← links)
- Verification of heap manipulating programs with ordered data by extended forest automata (Q300414) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- Verifying pointer safety for programs with unknown calls (Q604389) (← links)
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) (Q832157) (← links)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms (Q832310) (← links)
- Automata-based verification of programs with tree updates (Q845236) (← links)
- VST-Floyd: a separation logic tool to verify correctness of C programs (Q1663238) (← links)
- Nested antichains for WS1S (Q1733101) (← links)
- A relational shape abstract domain (Q2058389) (← links)
- Reasoning about block-based cloud storage systems via separation logic (Q2087457) (← links)
- A learning-based approach to synthesizing invariants for incomplete verification engines (Q2208307) (← links)
- Automated mutual induction proof in separation logic (Q2414251) (← links)
- Completeness and expressiveness of pointer program verification by separation logic (Q2417849) (← links)
- Forest automata for verification of heap manipulation (Q2441715) (← links)
- A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints (Q2817951) (← links)
- Invariants Synthesis over a Combined Domain for Automated Program Verification (Q2842643) (← links)
- Crowfoot: A Verifier for Higher-Order Store Programs (Q2891407) (← links)
- Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic (Q2988661) (← links)
- Featherweight VeriFast (Q3196351) (← links)
- Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation (Q3297594) (← links)
- Lazy Automata Techniques for WS1S (Q3303905) (← links)
- Disproving Inductive Entailments in Separation Logic via Base Pair Approximation (Q3455777) (← links)
- Lightweight Separation (Q3543659) (← links)
- Beyond Shapes: Lists with Ordered Data (Q3617745) (← links)
- (Q5111651) (← links)
- Automated Cyclic Entailment Proofs in Separation Logic (Q5200020) (← links)
- Certified Reasoning with Infinity (Q5206958) (← links)
- Automated Verification of Shape and Size Properties Via Separation Logic (Q5452612) (← links)
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions (Q5875940) (← links)
- Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure (Q5918382) (← links)