8 citations · 25 across the 18 of their papers we have counts for
10 papers · 1 filter
Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
Wanyun Su, Zhilin Wu, Mihaela Sighireanu
Pointer arithmetic is widely used in low-level programs, e.g. memory allocators. The specification of such programs usually requires using pointer arithmetic inside inductive defin…
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
Taolue Chen, Matthew Hague, Jinlong He +4
Strings are widely used in programs, especially in web applications. Integer data type occurs naturally in string-manipulating programs, and is frequently used to refer to lengths…
Monadic Decomposition in Integer Linear Arithmetic (Technical Report)
Matthew Hague, Anthony Widjaja Lin, Philipp Rümmer +1
Monadic decomposability is a notion of variable independence, which asks whether a given formula in a first-order theory is expressible as a Boolean combination of monadic predicat…
Separation Logic with Linearly Compositional Inductive Predicates and Set Data Constraints
Chong Gao, Taolue Chen, Zhilin Wu
We identify difference-bound set constraints (DBS), an analogy of difference-bound arithmetic constraints for sets. DBS can express not only set constraints but also arithmetic con…
What Is Decidable about String Constraints with the ReplaceAll Function
Taolue Chen, Yan Chen, Matthew Hague +2
Recently, it was shown that any theory of strings containing the string-replace function (even the most restricted version where pattern/replacement strings are both constant strin…
On Automated Lemma Generation for Separation Logic with Inductive Definitions
Constantin Enea, Mihaela Sighireanu, Zhilin Wu
Separation Logic with inductive definitions is a well-known approach for deductive verification of programs that manipulate dynamic data structures. Deciding verification condition…