Programming Languages and Systems
From MaRDI portal
Publication:5493374
DOI10.1007/11575467zbMath1159.68363MaRDI QIDQ5493374
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)
Related Items
Program Verification with Separation Logic, Completeness for recursive procedures in separation logic, Concise Read-Only Specifications for Better Synthesis of Programs with Pointers, A First-Order Logic with Frames, 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), Automated Theorem Proving for Assertions in Separation Logic with All Connectives, Decision Procedure for Entailment of Symbolic Heaps with Arrays, Disproving Inductive Entailments in Separation Logic via Base Pair Approximation, Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic, Completeness for a First-Order Abstract Separation Logic, Generalized arrays for Stainless frames, 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, Unnamed Item, Completeness and expressiveness of pointer program verification by separation logic, Proof tactics for assertions in separation logic, An efficient cyclic entailment procedure in a fragment of separation logic, Using Unified Model Checking to Verify Heaps, Foundations for entailment checking in quantitative separation logic, An algebraic glimpse at bunched implications and separation logic, Reasoning about sequences of memory states, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, 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, Strong-separation logic, A program logic for resources, Verify heaps via unified model checking, A generic framework for symbolic execution: a coinductive approach, Symbolic execution based on language transformation, Automatic verification of Java programs with dynamic frames, Unnamed Item, Matching Logic: An Alternative to Hoare/Floyd Logic, Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps, Unifying separation logic and region logic to allow interoperability, Access Analysis-Based Tight Localization of Abstract Memories, Unnamed Item, A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints, Non-well-founded deduction for induction and coinduction, Automatic Parallelization and Optimization of Programs by Proof Rewriting, An adaptation-complete proof system for local reasoning about cloud storage systems, Reasoning about block-based cloud storage systems via separation logic, Separation Logic Tutorial, Separation Logic Contracts for a Java-Like Language with Fork/Join, A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
