Programming Languages and Systems
From MaRDI portal
Publication:5493374
DOI10.1007/11575467zbMATH Open1159.68363MaRDI QIDQ5493374FDOQ5493374
Authors: Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn 
Publication date: 20 October 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Recommendations
Cited In (55)
- Restriction on cut rule in cyclic-proof system for symbolic heaps
- An algebraic glimpse at bunched implications and separation logic
- Completeness of cyclic proofs for symbolic heaps with inductive definitions
- Automated theorem proving for assertions in separation logic with all connectives
- Verify heaps via unified model checking
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- Foundations for entailment checking in quantitative separation logic
- Runtime Checking for Separation Logic
- Title not available (Why is that?)
- 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
- Make flows small again: revisiting the flow framework
- Lightweight Separation
- Matching logic: an alternative to Hoare/Floyd logic
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- Decision Procedure for Entailment of Symbolic Heaps with Arrays
- Concise read-only specifications for better synthesis of programs with pointers
- A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
- A program logic for resources
- Model Checking Software
- Title not available (Why is that?)
- Completeness and expressiveness of pointer program verification by separation logic
- 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
- 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
- Separation Logic Tutorial
- Automated mutual induction proof in separation logic
- Generating inductive predicates for symbolic execution of pointer-manipulating programs
- An efficient cyclic entailment procedure in a fragment of separation logic
- A generic framework for symbolic execution: a coinductive approach
- Proof tactics for assertions in separation logic
- Automatic Parallelization and Optimization of Programs by Proof Rewriting
- Proof automation for functional correctness in separation logic
- A complete decision procedure for linearly compositional separation logic with data constraints
- Completeness for a first-order abstract separation logic
- An adaptation-complete proof system for local reasoning about cloud storage systems
- Strong-separation logic
- A first-order logic with frames
- Crowfoot: A Verifier for Higher-Order Store Programs
- 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
- Access analysis-based tight localization of abstract memories
- Unified reasoning about robustness properties of symbolic-heap separation logic
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)
