Range allocation for separation logic

DOI10.1007/978-3-540-27813-9_12MaRDI QIDQ5312895zbMATH OpenOpenAlexFDO

Authors Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli

Publication date 25 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b98490

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• The SAT-based approach to separation logic
• Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
• Range allocation for equivalence logic
• A decision procedure for separation logic in SMT
• A separation logic with data: small models and automation

Cited in

(9)

• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Range allocation for equivalence logic
• Deciding separation formulas with SAT
• Proving Termination with (Boolean) Satisfaction
• Tools and Algorithms for the Construction and Analysis of Systems
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Local Search for SMT on Linear Integer Arithmetic
• Local search for solving satisfiability of polynomial formulas
• The SAT-based approach to separation logic

This page was built for publication: Range allocation for separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5312895)