HIP

swMATH9786MaRDI QIDQ21765

No author found.

Related Items (32)

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

This page was built for software: HIP