Separation logic (SL) is a widely used formalism for verifying programs that manipulate dynamically allocated memory, relying on the separating conjunction \(\star \) to combine disjoint heap structures. The standard approach in SL lacks the expressive power to handle overlaid data structures where multiple structures share some locations. We consider a logic that extends SL with a new separating conjunction operator , enabling the composition of heaps with shared locations that allocate distinct fields. Our fragment supports generic inductive definitions and introduces set variables to constrain the locations shared by overlapping structures. We prove that the satisfiability problem for this fragment is in Nexptime, by reducing it to the satisfiability problem in BAPA [11], a decidable logic combining Boolean algebra of sets and Presburger arithmetic.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Deciding Satisfiability for Overlaid Symbolic Heaps

  • Nicolas Peltier,
  • Quentin Petitjean,
  • Mihaela Sighireanu

摘要

Separation logic (SL) is a widely used formalism for verifying programs that manipulate dynamically allocated memory, relying on the separating conjunction \(\star \) to combine disjoint heap structures. The standard approach in SL lacks the expressive power to handle overlaid data structures where multiple structures share some locations. We consider a logic that extends SL with a new separating conjunction operator , enabling the composition of heaps with shared locations that allocate distinct fields. Our fragment supports generic inductive definitions and introduces set variables to constrain the locations shared by overlapping structures. We prove that the satisfiability problem for this fragment is in Nexptime, by reducing it to the satisfiability problem in BAPA [11], a decidable logic combining Boolean algebra of sets and Presburger arithmetic.