Constraint-Based Program Reasoning with Heaps and Separation

No abstract is available for this paper.

• Publication year

  2013

• Venue

  International Conference on Principles and Practice of Constraint Programming

• Publication date

  2013-09-16

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/978-3-642-40627-0_24
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Memory Efficient Data Structures for Explicit Verification of Timed Systems

  2014cited by this paper
• Theory and Practice of Logic Programming

  2014cited by this paper
• Axiomatic Basis for Computer Programming

  2013influential reference
• SMCHR: Satisfiability modulo constraint handling rules

  2012influential reference
• Formal Methods for Components and Objects: 10th International Symposium FMCO 2011, revised selected papers

  2012cited by this paper
• Decision Procedures for Region Logic

  2012cited by this paper
• VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java

  2011cited by this paper
• A machine program for theorem-proving

  2011cited by this paper
• Lazy Annotation for Program Testing and Verification

  2010cited by this paper
• An Interpolation Method for CLP Traversal

  2009cited by this paper
• Synthesizing Filtering Algorithms for Global Chance-Constraints

  2009cited by this paper
• ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genoa, Italy, July 6-10, 2009. Proceedings

  2009cited by this paper
• Propagation via lazy clause generation

  2009cited by this paper
• Separation Logic Verification of C Programs with an SMT Solver

  2009cited by this paper
• Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic

  2009cited by this paper
• Amortised Memory Analysis Using the Depth of Data Structures

  2009cited by this paper
• A Coinduction Rule for Entailment of Recursively Defined Properties

  2008cited by this paper
• ECOOP 2008 - Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 7-11, 2008, Proceedings

  2008cited by this paper
• Regional Logic for Local Reasoning about Global Invariants

  2008cited by this paper
• Automated Verification of Shape and Size Properties Via Separation Logic

  2007cited by this paper
• Compositional Class Refinement in Object-Z

  2006cited by this paper
• Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions

  2006cited by this paper
• A Fast Linear-Arithmetic Solver for DPLL(T)

  2006cited by this paper
• Smallfoot: Modular Automatic Assertion Checking with Separation Logic

  2005cited by this paper
• Symbolic Execution with Separation Logic

  2005influential reference
• Analysis of Recursive Game Graphs Using Data Flow Equations

  2004cited by this paper
• Verification: Theory and Practice

  2004cited by this paper
• Combining Sets with Elements

  2003cited by this paper
• Separation logic: a logic for shared mutable data structures

  2002cited by this paper
• CHRv: A Flexible Query Language

  1998influential reference
• Theory and Practice of Constraint Handling Rules

  1998influential reference
• Constraint Logic Programming: A Survey

  1994influential reference
• Guarded commands, nondeterminacy and formal derivation of programs

  1975cited by this paper

• Thrust: A Prophecy-Based Refinement Type System for Rust

  2025cites this paper
• Program Verification via Predicate Constraint Satisfiability Modulo Theories

  2020cites this paper
• Shape Neutral Analysis of Graph-based Data-structures

  2018influential citation
• Local Reasoning on Recursive Data Structures

  2017influential citation
• Constraint Handling Rules - What Else?

  2015cites this paper
• Automatic induction proofs of data-structures in imperative programs

  2015cites this paper
• A Rule-based Verification Strategy for Array Manipulating Programs

  2015cites this paper
• Construcción de programas que manejan dinámicamente la memoria

  2015cites this paper
• Automatic Reasoning on Recursive Data-Structures with Sharing

  2015cites this paper
• Local Reasoning with First-Class Heaps, and a New Frame Rule

  2015influential citation
• Program Verification using Constraint Handling Rules and Array Constraint Generalizations

  2014cites this paper
• Verification of Programs by Combining Iterated Specialization with Interpolation

  2014cites this paper
• On Termination, Confluence and Consistent CHR-based Type Inference

  2014cites this paper
• Towards Memory Access Safety Analysis for Protected Environments

  2014cites this paper
• Parametric completeness for separation theories

  2014cites this paper
• Proietti A RULE-BASED VERIFICATION STRATEGY FOR ARRAY MANIPULATING PROGRAMS R . 7 2014

  2014cites this paper
• Proving Data Structure Properties by Automatic Induction

  2013cites this paper
• Under Consideration for Publication in Theory and Practice of Logic Programming on Termination, Confluence and Consistent Chr-based Type Inference

  year unknowncites this paper