Deciding separation formulas with SAT

DOI10.1007/3-540-45657-0_16MaRDI QIDQ4804898zbMATH OpenFDO

Authors Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant

Publication date 1 May 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2404/24040209.htm

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) 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
• Computer Aided Verification
• scientific article; zbMATH DE number 1979549
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures

Cited in

(18)

• A framework for satisfiability modulo theories
• Zero, successor and equality in BDDs
• Separating signs in the propositional satisfiability problem
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• SMELS: satisfiability modulo equality with lazy superposition
• The model evolution calculus as a first-order DPLL method
• Efficient theory combination via Boolean search
• Satisfiability modulo theories
• SAT-Based Formula Simplification
• Combining instance generation and resolution
• A term rewriting technique for decision graphs
• Exploiting symmetry in SMT problems
• Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Local Search for SMT on Linear Integer Arithmetic
• Beyond eager encodings: a theory-agnostic approach to theory-lemma enumeration in SMT
• The SAT-based approach to separation logic
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures

This page was built for publication: Deciding separation formulas with SAT

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