HIP

swMATH9786MaRDI QIDQ21765FDOQ21765

Author name not available (Why is that?)

Cited In (32)

• A learning-based approach to synthesizing invariants for incomplete verification engines
• 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
• Disproving inductive entailments in separation logic via base pair approximation
• Enhancing symbolic execution of heap-based programs with separation logic for test input generation
• Automata-based verification of programs with tree updates
• Completeness for recursive procedures in separation logic
• Automated Verification of Shape and Size Properties Via Separation Logic
• Symbolic execution proofs for higher order store programs
• Lightweight Separation
• 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
• Tractability of separation logic with inductive definitions: beyond lists
• Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure
• Automated cyclic entailment proofs in separation logic
• A relational shape abstract domain
• Automated mutual induction proof in separation logic
• A complete decision procedure for linearly compositional separation logic with data constraints
• 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
• Invariants synthesis over a combined domain for automated program verification
• Reasoning about block-based cloud storage systems via separation logic
• Certified reasoning with infinity
• Lazy automata techniques for WS1S
• Unified reasoning about robustness properties of symbolic-heap separation logic

This page was built for software: HIP