Separation logic and its variants can describe various properties on pointer
programs. However, when it comes to properties on sequences, one may find it
hard to formalize. To deal with properties on variable-length sequences and
multilevel data structures, we propose sequence-heap separation logic which
integrates sequences into logical reasoning on heap-manipulated programs.
Quantifiers over sequence variables and singleton heap storing sequence
(sequence singleton heap) are new members in our logic. Further, we study the
satisfiability problem of two fragments. The propositional fragment of
sequence-heap separation logic is decidable, and the fragment with 2
alternations on program variables and 1 alternation on sequence variables is
undecidable. In addition, we explore boundaries between decidable and
undecidable fragments of the logic with prenex normal form.

我们提出了序列堆分离逻辑，将序列集成到堆操纵程序的逻辑推理中，该逻辑包括序列变量量词和存储序列的单例堆。我们研究了序列堆分离逻辑的两个片段的可满足性问题，并探讨了正前式正规形式的解释逻辑边界。