A separation logic for sequences in pointer programs and its decidability
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Logical ReasoningSimilar Papers 제목 키워드 기반
On the Verification of Belief Programs
In a recent paper, Belle and Levesque proposed a framework for a type of program called belief programs, a probabilistic extension of GOLOG programs where every action and sensing result could be noisy and every test con…
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a full classification of FSAT depending on t…
RelationLeveraging Rust types for modular specification and verification
Rust's type system ensures memory safety: well-typed Rust programs are guaranteed to not exhibit problems such as dangling pointers, data races, and unexpected side effects through aliased references. Ensuring correctnes…
Formal LogicString Theories involving Regular Membership Predicates: From Practice to Theory and Back
Widespread use of string solvers in formal analysis of string-heavy programs has led to a growing demand for more efficient and reliable techniques which can be applied in this context, especially for real-world cases. D…
Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs
We present a novel sampling framework for probabilistic programs. The framework combines two recent ideas -- \emph{control-data separation} and \emph{logical condition propagation} -- in a nontrivial manner so that the t…
Bayesian Inference