Programming Languages and Systems
From MaRDI portal
Publication:5493374
Recommendations
Cited in
(55)- Unified reasoning about robustness properties of symbolic-heap separation logic
- Verify heaps via unified model checking
- Automated theorem proving for assertions in separation logic with all connectives
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- Foundations for entailment checking in quantitative separation logic
- Runtime Checking for Separation Logic
- scientific article; zbMATH DE number 7350781 (Why is no real title available?)
- Disproving inductive entailments in separation logic via base pair approximation
- Separation Logic Contracts for a Java-Like Language with Fork/Join
- Enhancing symbolic execution of heap-based programs with separation logic for test input generation
- Completeness for recursive procedures in separation logic
- Automatic verification of Java programs with dynamic frames
- Reasoning about sequences of memory states
- Using unified model checking to verify heaps
- Symbolic execution proofs for higher order store programs
- Symbolic execution based on language transformation
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Matching logic: an alternative to Hoare/Floyd logic
- Lightweight Separation
- Make flows small again: revisiting the flow framework
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- Concise read-only specifications for better synthesis of programs with pointers
- A program logic for resources
- 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
- scientific article; zbMATH DE number 7561347 (Why is no real title available?)
- Model Checking Software
- Verifying pointer safety for programs with unknown calls
- Program Verification with Separation Logic
- Generalized arrays for Stainless frames
- Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps
- Restriction on cut rule in cyclic-proof system for symbolic heaps
- Tractability of separation logic with inductive definitions: beyond lists
- Non-well-founded deduction for induction and coinduction
- Unifying separation logic and region logic to allow interoperability
- An algebraic glimpse at bunched implications and separation logic
- Separation Logic Tutorial
- Automated mutual induction proof in separation logic
- Generating inductive predicates for symbolic execution of pointer-manipulating programs
- A generic framework for symbolic execution: a coinductive approach
- Proof tactics for assertions in separation logic
- An efficient cyclic entailment procedure in a fragment of separation logic
- Automatic Parallelization and Optimization of Programs by Proof Rewriting
- Proof automation for functional correctness in separation logic
- An adaptation-complete proof system for local reasoning about cloud storage systems
- A complete decision procedure for linearly compositional separation logic with data constraints
- Completeness for a first-order abstract separation logic
- Strong-separation logic
- Crowfoot: A Verifier for Higher-Order Store Programs
- A first-order logic with frames
- Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- VST-Floyd: a separation logic tool to verify correctness of C programs
- Reasoning about block-based cloud storage systems via separation logic
- Completeness of cyclic proofs for symbolic heaps with inductive definitions
- Access analysis-based tight localization of abstract memories
This page was built for publication: Programming Languages and Systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5493374)
