HIP

swMATH9786MaRDI QIDQ21765FDOQ21765

Author name not available (Why is that?)

Cited In (32)

• A learning-based approach to synthesizing invariants for incomplete verification engines
• A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
• Nested antichains for WS1S
• Invariants Synthesis over a Combined Domain for Automated Program Verification
• Automata-based verification of programs with tree updates
• Completeness for recursive procedures in separation logic
• Title not available (Why is that?)
• Automated Verification of Shape and Size Properties Via Separation Logic
• Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
• Symbolic execution proofs for higher order store programs
• Lazy Automata Techniques for WS1S
• Lightweight Separation
• Automated Cyclic Entailment Proofs in Separation Logic
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Verification of heap manipulating programs with ordered data by extended forest automata
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• Completeness and expressiveness of pointer program verification by separation logic
• Verifying pointer safety for programs with unknown calls
• Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation
• Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
• Certified Reasoning with Infinity
• Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
• A relational shape abstract domain
• Automated mutual induction proof in separation logic
• Forest automata for verification of heap manipulation
• Featherweight VeriFast
• Beyond Shapes: Lists with Ordered Data
• Crowfoot: A Verifier for Higher-Order Store Programs
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Reasoning about block-based cloud storage systems via separation logic

This page was built for software: HIP