Word Embeddings to Enhance Twitter Gang Member Profile Identification

Gang affiliates have joined the masses who use social media to share thoughts and actions publicly. Interestingly, they use this public medium to express recent illegal actions, to intimidate others, and to share outrageous images and statements. Agencies able to unearth these profiles may thus be able to anticipate, stop, or hasten the investigation of gang-related crimes. This paper investigates the use of word embeddings to help identify gang members on Twitter. Building on our previous work, we generate word embeddings that translate what Twitter users post in their profile descriptions, tweets, profile images, and linked YouTube content to a real vector format amenable for machine learning classification. Our experimental results show that pre-trained word embeddings can boost the accuracy of supervised learning algorithms trained over gang members social media posts.

Introduction
Street gangs are defined as "a coalition of peers, united by mutual interests, with identifiable leadership and internal organization, who act collectively to conduct illegal activity and to control a territory, facility, or enterprise" [Mil92]. They promote criminal activities such as drug trafficking, assault, robbery, and threatening or intimidating a neighborhood [20113]. Today, over 1.4 million people, belonging to more than 33,000 gangs, are active in the United States [20111], of which 88% identify themselves as being members of a street gang 1 . They are also active users of social media [20111]; according to 2007 National Assessment Center's survey of gang members, 25% of individuals in gangs use the Internet for at least 4 hours a week [20007]. More recent studies report approximately 45% of gang members participate in online offending activities such as threatening, harassing individuals, posting violent videos or attacking someone on the street for something they said online [DP11,PDJ15]. They confirm that gang members use social media to express themselves in ways similar to their offline behavior on the streets [PEB13].
Despite its public nature, gang members post on social media without fear of consequences because there are only few tools law enforcement can presently use to surveil social media [WDSD15]. For example, the New York City police department employs over 300 detectives to combat teen violence triggered by insults, dares, and threats exchanged on social media, and the Toronto police department teaches officers about the use of social media in investigations [pol13]. From offline clues, the officers monitor just a selected set of social media accounts which are manually discovered and related to a specific investigation. Thus, developing tools to identify gang member profiles on social media is an important step in the direction of using machine intelligence to fight crime.
To help agencies monitor gang activity on social media, our past work investigated how features from Twitter profiles, including profile text, profile images, tweet text, emjoi use, and their links to YouTube, may be used to reliably find gang member profiles [BWDS16]. The diverse set of features, chosen to combat the fact that gang members often use local terms and hashtags in their posts, offered encouraging results. In this paper, we report our experience in integrating deep learning into our gang member profile classifier. Specifically, we investigate the effect of translating the features into a vector space using word embeddings [MSC + 13]. This idea is motivated by the recent success of word embeddings-based methods to learn syntactic and semantic structures automatically when provided with large datasets. A dataset of over 3,000 gang and non-gang member profiles that we previously curated is used to train the word embeddings. We show that pre-trained word embeddings improve the machine learning models and help us obtain an F 1score of 0.7835 on gang member profiles (a 6.39% improvement in F 1-score compared to the baseline models which were not trained using word embeddings).
This paper is organized as follows. Section 2 discusses the related literature and frames how this work differs from other related works. Section 3 discusses our approach based on word embeddings to identify gang member profiles. Section 4 reports on the evaluation of the proposed approach and the evaluation results in detail. Section 5 concludes the work reported while discussing the future work planned.

Related Work
Researchers have begun investigating the gang members' use of social media and have noticed the importance of identifying gang members' Twitter profiles a priori [PEB13,WDSD15]. Before analyzing any textual context retrieved from their social media posts, knowing that a post has originated from a gang member could help systems to better understand the message conveyed by that post. Wijeratne et al. developed a framework to analyze what gang members post on social media [WDSD15]. Their framework could only extract social media posts from self identified gang members by searching for pre-identified gang names in a user's Twitter profile description. Patton et al. developed a method to collect tweets from a group of gang members operating in Detroit, MI [Pat15]. However, their approach required the gang members' Twitter profile names to be known beforehand, and data collection was localized to a single city in the country. These studies investigated a small set of manually curated gang member profiles, often from a small geographic area that may bias their findings.
In our previous work [BWDS16], we curated what may be the largest set of gang member profiles to study how gang member Twitter profiles can be automatically identified based on the content they share online. A data collection process involving location neutral keywords used by gang members, with an expanded search of their retweet, friends and follower networks, led to identifying 400 authentic gang member profiles on Twitter. Our study discovered that the text in their tweets and profile descriptions, their emoji use, their profile images, and music interests embodied by links to YouTube music videos, can help a classifier distinguish between gang and non-gang member profiles. While a very promising F 1 measure with low false positive rate was achieved, we hypothesize that the diverse kinds and the multitude of features employed (e.g. unigrams of tweet text) could be amenable to an improved representation for classification. We thus explore the possibility of mapping these features into a considerably smaller feature space through the use of word embeddings.
Previous research has shown word embeddingsbased methods can significantly improve short text classification [WXX + 16, LZZ15]. For example, Lilleberget et al. showed that word embeddings weighted by tf -idf outperforms other variants of word embedding models discussed in [LZZ15], after training word embedding models on over 18,000 newsgroup posts. Wang et al. showed that short text categorization can be improved by word embeddings with the help of a neural network model that feeds semantic cliques learned over word embeddings in to a convolutions neural network [WXX + 16]. We believe our corpus of gang and non-gang member tweets, with nearly 64.6 million word tokens, could act as a rich resource to train word embeddings for distinguishing gang and non-gang member Twitter users. Our investigation differs from other word embeddings-based text classification systems such as [WXX + 16, LZZ15] due to the fact that we use multiple feature types including emojis in tweets and image tags extracted from Twitter profile and cover images in our classification task.

Word Embeddings
A word embedding model is a neural network that learns rich representations of words in a text corpus. It takes data from a large, n-dimensional 'word space' (where n is the number of unique words in a corpus) and learns a transformation of the data into a lower k-dimensional space of real numbers. This transformation is developed in a way that similarities between the k-dimensional vector representation of two words reflects semantic relationships among the words themselves. These semantics are not captured by typical bag-of-words or n-gram models for classification tasks on text data [MYZ13, MSC + 13].
Word embeddings have led to the state-of-the-art results in many sequential learning tasks [LBH15]. In fact, word embedding learning is an important step for many statistical language modeling tasks in text processing systems. Bengio et al. were the first ones to introduce the idea of learning a distributed representation for words over a text corpus [BDVJ03]. They learned representations for each word in the text corpus using a neural network model that modeled the joint probability function of word sequences in terms of the feature vectors of the words in the sequence. Mikolov et al. showed that simple algebraic operations can be performed on word embeddings learned over a text corpus, which leads to findings such as the word embedding vector of the word "King" − the word embedding vectors of "Man" + "Woman" would results in a word embedding vector that is closest to the word embedding vector of the word "Queen" [MYZ13]. Recent successes in using word embeddings to improve text classification for short text [WXX + 16, LZZ15], encouraged us to explore how they can be used to improve gang and non-gang member Twitter profile classification.
Word embeddings can be performed under different neural network architectures; two popular ones are the Continuous Bag-of-Words (CBOW) and Continuous Skip-gram (Skip-gram) models [MCCD13]. The CBOW model learns a neural network such that given a set of context words surrounding a target word, it predict a target word. The Skip-gram model differs by predicting context words given a target word and by capturing the ordering of word occurrences. Recent improvements to Skip-gram model make it better able to handle less frequent words, especially when negative sampling is used [MSC + 13].

Features considered
Gang member tweets and profile descriptions tend to have few textual indicators that demonstrate their gang affiliations or their tweets/profile text may carry acronyms which can only be deciphered by others involved in gang culture [BWDS16]. These gang-related terms are often local to gangs operating in neighborhoods and change rapidly when they form new gangs. Consequently, building a database of keywords, phrases, and other identifiers to find gang members nationally is not feasible. Instead, we use heterogeneous sets of features derived not only from profile and tweet text but also from the emoji usage, profile images, and links to YouTube videos reflecting their music preferences and affinity. In this section, we briefly discuss the feature types and their broad differences in gang and non-gang member profiles. An in-depth explanation of these feature selection can be found in [BWDS16].
1. Tweet text: In our previous work, we observed that gang members use curse words nearly five times more than the average curse words use on Twitter [BWDS16]. Further, we noticed that gang members mainly use Twitter to discuss drugs and money using terms such as smoke, high, hit, money, got, and need while non-gang members mainly discuss their feelings using terms such as new, like, love, know, want, and look.
2. Twitter profile description: We found gang member profile descriptions to be rife with curse words (nigga, fuck, and shit) while non-gang members use words related to their feelings or interests (love, life, music, and book). We noticed that gang members use their profile descriptions as a space to grieve for their fallen or incarcerated gang members as about 12% of gang member Twitter profiles used terms such as rip and free.

Emoji features:
We found that the fuel pump emoji was the most frequently used emoji by gang members, which is often used in the context of selling or consuming marijuana. The pistol emoji was the second most frequently used emoji, which is often used with the police cop emoji in an 'emoji chain' to express their hatred towards law enforcement officers. The money bag emoji, money with wings emoji, unlock emoji, and a variety of the angry face emoji such as the devil face emoji and imp emoji were also common in gang members' but not in non-gang members' tweets.
4. Twitter profile and cover images: We noticed that gang members often pose holding or pointing weapons, seen in a group fashion which displays a gangster culture, show off graffiti, hand signs, tattoos, and bulk cash in their profile and cover images. We used Clarifai web service 2 to tag the profile and cover images of the Twitter users in our dataset and used the image tags returned by Clarifai API to train word embeddings. Tags such as trigger, bullet, and worship were unique for gang member profiles while non-gang member images had unique tags such as beach, seashore, dawn, wildlife, sand, and pet.

YouTube videos:
We found that 51.25% of the gang members in our dataset have a tweet that links to a YouTube video. Further, we found that 76.58% of the shared links are related to hip-hop music, gangster rap, and the culture that surrounds this music genre [BWDS16]. Moreover, we found that eight YouTube links are shared on average by a gang member. The top 5 terms used in YouTube videos shared by gang members were shit, like, nigga, fuck, and lil while like, love, peopl, song, and get were the top 5 terms in nongang members' video data. Figure 1 gives an overview of the steps to learn word embeddings and to integrate them into a classifier. We first convert any non-textual features such as emoji and profile images into textual features. We use Emoji for Python 3 and Clarifai services, respectively, to convert emoji and images into text. Prior to training the word embeddings, we remove all the seed words used to find gang member profiles and stopwords, and perform stemming across all tweets and profile descriptions. We then feed all the training data (word w t in Figure 1) we collected from our Twitter dataset to Word2Vec tool and train it using a Skip-gram model with negative sampling. When training the Skip-gram model, we set the negative sampling rate to 10 sample words, which seems to work well with medium-sized datasets [MSC + 13]. We set the context word window to be 5, so that it will consider 5 words to left and right of the target word (words w t−5 to w t+5 in Figure 1). This setting is suitable for sentences where average sentence length is less than 11 words, as is the case in tweets [HTK13]. We ignore the words that occur less than 5 times in our training corpus. We investigated how well the local language has been captured by the word embedding models we trained. We used the 'most similar' functionality offered by Word2Vec tool to understand what the model has learned about few gang-related slang terms which are specific to Chicago area. For example, we analyzed the ten most similar words learned by the word embedding model for the term BDK (Black Desciples Killers). We noticed that out of the 10 most similar words, five were names of local Chicago gangs, which are rivals of the Black Disciples Gang, two were different syntactic variations of BDK (bdkk, bdkkk) and the other three were different syntactic variations of GDK (gdk, gdkk, gdkkk). GDK is a local gang slang for 'Gangster Disciples Killer' which is used by rivals of Gangster Disciples gang to show their hatred towards them. We found similar results for the term GDK. Out of the ten most similar words, six were showing hatred towards six different Gangster Disciples gangs that operate in Chicago area. We believe that those who used the term GDK to show their hatred towards Gangster Disciples gangs might be also having rivalry with the six gangs we found.

Classification approach
We obtain word vectors of size 300 from the learned word embeddings. To represent a Twitter profile, we retrieve word vectors for all the words that appear in a particular profile including the words appear in tweets, profile description, words extracted from emoji, cover and profile images converted to textual formats, and words extracted from YouTube video comments and 3 https://pypi.python.org/pypi/emoji/  descriptions for all YouTube videos shared in the user's timeline. Those word vectors are combined to compute the final feature vector for the Twitter profile. To combine the word vectors, we consider five different methods. Letting the size of a word vector be k = 300, for a Twitter profile p with n unique words and the vector of the i th word in p denoted by w ip , we compute the feature vector for the Twitter profile V p by: 1. Sum of word embeddings V psum . This is the sum the word embedding vectors obtained for all words in a Twitter profile: Mean of word embeddings V pavg . This is the mean of the word embedding vectors of all words found in a Twitter profile: 3. Sum of word embeddings weighted by term frequency V p sum(count) . This is each word embedding vector multiplied by the word's frequency for the Twitter profile: where c ip is the term frequency for the i th word in profile p.

Sum of word embeddings weighted by
. This is each word vector multiplied by the word's tf -idf for the Twitter profile: where t ip is the tf -idf value for the i th word in profile p. 5. Mean of word embeddings weighted by term frequency V p avg(sum(count)) . This is the mean of the word embedding vectors weighted by term frequency:

Evaluation
We evaluate the performance of using word embeddings to discover gang member profiles on Twitter.
We first discuss the dataset, learning algorithms and baseline comparison models used in the experiments. Then we discuss the 10-fold cross validation experiments and the evaluation matrices used. Finally we present the results of the experiments.

Evaluation setup
We consider a dataset of curated gang and non-gang members' Twitter profiles collected from our previous work [BWDS16]. It was developed by querying the Followerwonk Web service API 4 with location-neutral seed words known to be used by gang members across the U.S. in their Twitter profiles. The dataset was further expanded by examining the friends, follower, and retweet networks of the gang member profiles found by searching for seed words. Specific details about our data curation procedure are discussed in [BWDS16]. Ultimately, this dataset consists of 400 gang member profiles and 2,865 non-gang member profiles. For each user profile, we collected up to most recent 3,200 tweets from their Twitter timelines, profile description text, profile and cover images, and the comments and video descriptions for every YouTube video shared by them. Table 1 provides statistics about the number of words found in each type of feature in the dataset. It includes a total of 821,412 tweets from gang members and 7,238,758 tweets from non-gang members.
To build the classifiers we used three different learning algorithms, namely Logistic Regression (LR), Random Forest (RF), and Support Vector Machines 4 https://moz.com/followerwonk/bio (SVM). We used version 0.17.1 of scikit-learn 5 machine learning library for Python to implement the classifiers. An open source tool of Python, Gensim [ŘS10] was used to generate the word embeddings. We compare our results with the two best performing systems reported in [BWDS16] which are the two state-of-theart models for identifying gang members in Twitter. Both baseline models are built from a random forest classifier trained over term frequencies for unigrams in tweet text, emoji, profile data, YouTube video data and image tags. Baseline Model(1) considers all 3,285 gang and non-gang member profiles in our dataset. Baseline Model(2) considers all Twitter profiles that contain every feature type discussed in Section 3.1. Because a Twitter profile may not have every feature type, baseline Model(1) represents a practical scenario where not every Twitter profile contains every type of feature. However, we compare our results to both baseline models and report the improvements.

10-fold cross validation
We conducted 10-fold cross validation experiments to evaluate the performance of our models. We used all Twitter profiles in the dataset to conduct experiments on the five methods we used to combine word embedding vectors. For each of the five vector combination methods (as mentioned in Section 3.2), we trained classifiers using each learning algorithm we considered. In each fold, the training set was used to generate the word vectors, which were then used to compute features for both the training set and test set. For each 10-fold cross validation experiment, we report three evaluation metrics for the 'gang' (positive) and 'non-gang' (negative) classes, namely, the Precision = tp/(tp + f p), Recall = tp/(tp + f n), and F 1-score = 2 * (P recision * Recall)/(P recision + Recall), where tp is the number of true positives, f p is the number of false positives, tn is the number of true negatives, and f n is the number of false negatives. We report these metrics for the 'gang' and 'non-gang' classes separately because of the class imbalance in the dataset. Table 2 presents 10-fold cross validation results for the baseline models (first and second rows) and our word embeddings-based models (from third row to seventh row). As mentioned earlier both baseline models use a random forest classifier trained on term frequencies of unigram features extracted from all feature types. The two baseline models only differs on the training data filtering method used, which is based on the availability of features in the training dataset as described

Model Classifier
Gang Non-Gang Precision Recall F 1-score   [BWDS16]. The baseline Model(1) uses all profiles in the dataset and has a F 1-score of 0.7364 for 'gang' class and 0.9690 for 'non-gang' class. The baseline Model(2) which only uses profiles that contain each and every feature type has a F 1-score of 0.7755 for 'gang' class and F 1-score of 0.9720 for 'non-gang' class.
Vector sum is one of the basic operations we can perform on word embedding vectors. The random forest classifier performs the best among vector sumbased classifiers where logistic regression and SVM classifiers also perform comparatively well (V psum ). Using vector mean (V pavg ) improves all classifier results and SVM classifier trained on the mean of word embeddings achieves very close results to the baseline Model(2). Multiplying vector sum with corresponding word counts for each word in word embeddings degrades the classifier accuracy for correctly identifying the positive class (V p sum(count) ). When we multiply words by their corresponding tf -idf values before taking the vector sum, we again observe an increase in the classifiers' accuracy (V p sum(tf −idf ) ). We achieve the best performance by averaging the vector sum weighted by term frequency (V p avg(sum(count)) ). Here we multiply the mean of the word embeddings by count of each word, which beats all other word embeddingsbased models and the two baselines. In this setting, logistic regression classifier trained on word embeddings performs the best with a F 1-score of 0.7835. This is a 6.39% improvement in performance when compared to the baseline Model(1) and a 1.03% improvement in performance when compared to baseline Model(2). Overall, out of the five vector operations that we used to train machine learning classifiers, four gave us classifier models that beat baseline Model(1) and two vector based operations gave us classifier models that either achieved very similar results to baseline Model(2) or beat it. This evaluation demonstrates the promise of using pre-trained word embeddings to boost the accuracy of supervised learning algorithms for Twitter gang member profile classification.

Conclusion and Future Work
This paper presented a word embeddings-based approach to address the problem of automatically identifying gang member profiles on Twitter. Using a Twitter user dataset that consist of 400 gang member and 2,865 non gang member profiles, we trained word embedding models based on users' tweets, profile descriptions, emoji, images, and videos shared on Twitter (textual features extracted from images, and videos). We then use the pre-trained word embedding models to train supervised machine learning classifiers, which showed superior performance when compared to the state-of-the-art baseline models reported in the literature. We plan to further extend our work by building our own image classification system specifically designed to identify images commonly shared by gang members such as guns, gang hand signs, stacks of cash and drugs. We would also like to experiment with automatically building dictionaries that contain gang names and gang-related slang using crowd-sourced gang-related knowledge-bases such as HipWiki 6 . We also want to experiment with using such knowledge-bases to train word embeddings to understand whether having access to gang-related knowledge could boost the performance of our models.
Finally, we would like to study how we can further use social networks of known gang members to identify new gang member profiles on Twitter.


A Decision Procedure for Separation Logic in SMT

This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic ($\seplog$) interpreted over heaplets with data elements ranging over a parametric multi-sorted (possibly infinite) domain. The algorithm uses a combination of theories and is used as a specialized solver inside a DPLL($T$) architecture. A prototype was implemented within the CVC4 SMT solver. Preliminary evaluation suggests the possibility of using this procedure as a building block of a more elaborate theorem prover for SL with inductive predicates, or as back-end of a bounded model checker for programs with low-level pointer and data manipulations.

Introduction
Separation Logic (SL) [21] is a logical framework for describing dynamically allocated mutable data structures generated by programs that use pointers and low-level memory allocation primitives. The logics in this framework are used by a number of academic (Space Invader [5], Sleek [17]), and industrial (Infer [8]) tools for program verification. The main reason for chosing to work within the SL framework is its ability to provide compositional proofs of programs, based on the principle of local reasoning: analyzing different parts of the program (e.g. functions, threads), that work on disjoint parts of the global heap, and combining the analysis results a-posteriori.
The main ingredients of SL are (i) the separating conjunction φ * ψ, which asserts that φ and ψ hold for separate portions of the memory (heap), (ii) the magic wand ϕ ⊸ ψ, which asserts that any extension of the heap by a disjoint heap that satisfies φ must satisfy ψ, and (iii) the frame rule, that exploits separation to provide modular reasoning about programs. Consider, for instance, a memory configuration (heap), in which two cells are allocated, and pointed to by the program variables x and y, respectively, where the x cell has an outgoing selector field to the y cell, and viceversa. The heap can be split into two disjoint parts, each containing exactly one cell, and described by an atomic proposition x → y and y → x, respectively. Then the entire heap is described by the formula x → y * y → x, which reads x points to y and separately y points to x.
The expressive power of SL comes with an inherent difficulty of automatically reasoning about the satisfiability of its formulae, as required by push-button program analysis tools. Indeed, SL becomes undecidable in the presence of first-order quantification, even when the fragment uses only points-to predicates, without the separating conjunction or the magic wand [9]. Moreover, the quantifier-free fragment with no data constraints, using only points-to predicates x → (y, z), where x, y and z are interpreted as Regarding SL with fixed inductive predicates, Perez and Rybalchenko [16] define a theorem proving framework relying on a combination of SL inference rules dealing with singly-linked lists only, and a superposition calculus dealing with equalities and aliasing between variables. Concerning SL with generic user-provided inductive predicates, the theorem prover Sleek [17] implements a semi-algorithmic entailment check, based on unfoldings and unifications. Along this line of work, the theorem prover Cyclist [7] builds entailment proofs using a sequent calculus. More recently, the tool Slide [14] reduces the entailment between inductive predicates to an inclusion between tree automata. The great majority of these inductive provers focus on applying induction strategies efficiently, and consider a very simple fragment of non-inductive SL formulae, typically conjunctions of equalities and disequalities between location variables and separated points-to predicates, without negations or the magic wand. On a more general note, the tool Spen [10] considers also arithmetic constraints between the data elements in the memory cells, but fixes the shape of the user-defined predicates.
The idea of applying SMT techniques to decide satisfiability of SL formulae is not new. In their work, Piskac, Wies and Zufferey translate from SL with singly-linked list segments [18] and trees [?], respectively, into first-order logics (Grass and Grit) that are decidable in NP. The fragment handled in this paper is incomparable to the logics Grass [18] and Grit [?]. On one hand, we do not consider predicates defining recursive data structures, such as singly-linked lists. On the other hand, we deal with the entire quantifier-free fragment of SL, including arbitrary nesting of the magic wand, separating conjunction and classical boolean connectives. As a result, the decision problem we consider is PSPACE-complete, due to the possibility of arbitrary nesting of the boolean and SL connectives. To the best of our knowledge, our implementation is also the first to enable theory combination involving SL, in a fine-grained fashion, directly within the DPLL(T ) loop. Indeed, we do not translate SL into classical multi-sorted logic upfront, but rather use lazy evaluation and counterexample-driven quantifier instantiation, that can solve non-trivial instances of the satisfiability problem efficiently.
The first theoretical results on decidability and complexity of SL without inductive predicates are given by Calcagno, Yang and O'Hearn [9]. They show that the quantifierfree fragment of SL without data constraints is PSPACE-complete by an argument that enumerates a finite (yet large) set of heap models. Their argument shows also the difficulty of the problem, however it cannot be directly turned into an effective decision procedure, because of the ineffectiveness of model enumeration. A more elaborate tableaubased decision procedure is described by Méry and Galmiche [11]. This procedure generates verification conditions on-demand, but here no data constraints are considered, either. However, combined, the results of [9] and [11] have inspired our decision procedure, that is parameterized by a decidable quantifier-free fragment of a base theory, and can be used in combination with any available SMT theory.
Our procedure relies on a decision procedure for quantifier-free parametric theory of sets and on-demand techniques for quantifier instantiation. Decision procedures for the theory of sets in SMT are given in [22,1]. Techniques for model-driven quantifier instantiation were introduced in the context of SMT in [13], and have been developed recently in [19,6].

Preliminaries
We consider formulae in multi-sorted first-order logic, over a signature Σ consisting of a countable set of sort symbols and a set of function symbols. We assume that signatures always include a boolean sort Bool with constants ⊤ and ⊥ denoting true and false respectively, and that each sort σ is implicitly equipped with an equality predicate ≈ over σ × σ. Moreover, we may assume without loss of generality that equality is the only predicate belonging to Σ, since we can model other predicate symbols as function symbols with return sort Bool 4 .
We consider a set x of first-order variables, with associated sorts, and denote by ϕ(x) the fact that the free variables of the formula ϕ belong to x. Given a signature Σ, well-sorted terms, atoms, literals, and formulae are defined as usual, and referred to respectively as Σ-terms. We denote by φ[ϕ] the fact that ϕ is a subformula (subterm) of φ and by φ[ψ/ϕ] the result of replacing ϕ with ψ in φ. We write ∀x.ϕ to denote universal quantification over variable x, where x occurs as a free variable in ϕ. If x = x 1 , . . . , x n is a tuple of variables, we write ∀.x ϕ as an abbreviation of ∀.x 1 · · · ∀x n ϕ. We say that a Σ-term is ground if it contains no free variables. We assume Σ contains an if-then-else operator ite(b, t, u), of sort Bool × σ × σ → σ, for each sort σ, that evaluates to t if b = ⊤ and to u otherwise.
A Σ-interpretation I maps:(i) each set sort symbol σ ∈ Σ to a non-empty set σ I , the domain of σ in I, (ii) each function symbol f ∈ Σ of sort σ 1 × . . . × σ n → σ to a total function f I of sort σ I 1 × . . . × σ I n → σ I if n > 0, and to an element of σ I if n = 0, and (iii) each variable x ∈ x to an element of σ I x , where σ x is the sort symbol associated with x. We denote by t I the interpretation of a term t induced by the mapping I. The satisfiability relation between Σ-interpretations and Σ-formulae, written I | = ϕ, is defined inductively, as usual. We say that I is a model of ϕ if I | = ϕ.
A first-order theory is a pair T = (Σ, I) where Σ is a signature and I is a nonempty set of Σ-interpretations, the models of T . For a formula ϕ, we denote by A formula ϕ T -entails a Σ-formula φ, written ϕ | = T φ, if every model of T that satisfies ϕ also satisfies φ. The formulae ϕ and ψ are T -equivalent if ϕ | = T φ and φ | = T ϕ, and equisatisfiable (in T ) if ψ is T -satisfiable if and only if ϕ is T -satisfiable. Furthermore, formulas ϕ and ψ are equivalent (up to k) if they are satisfied by the same set of models (when restricted to the interpretation of variables k). The T -satisfiability problem asks, given a Σ-formula ϕ, whether [[ϕ]] T ∅, i.e. whether ϕ has a T -model.

Separation Logic
In the remainder of the paper we fix a theory T = (Σ, I), such that the T -satisfiability for the language of quantifier-free boolean combinations of equalities and disequalties between Σ-terms is decidable. We fix two sorts Loc and Data from Σ, with no restriction other than the fact that Loc is always interpreted as a countably infinite set. We refer to Separation Logic for T , written SL (T ), as the set of formulae generated by the syntax: where t and u are well-sorted Σ-terms and that for any atomic proposition t → u, t is of sort Loc and u is of sort Data. Also, we consider that Σ has a constant nil of sort Loc, with the intended meaning that t → u never holds when t ≈ nil. In the following, we write φ ∨ ψ for ¬(¬φ ∧ ¬ψ) and φ ⇒ ψ for ¬φ ∨ ψ.
Given an interpretation I, a heap is a finite partial mapping h : Loc I ⇀ fin Data I . For a heap h, we denote by dom(h) its domain. For two heaps h 1 and h 2 , we write h 1 #h 2 for dom(h 1 ) ∩ dom(h 2 ) = ∅ and h = h 1 ⊎ h 2 for h 1 #h 2 and h = h 1 ∪ h 2 . For an interpretation I, a heap h : Loc I ⇀ fin Data I and a SL(T ) formula φ, we define the satisfaction relation I, h | = SL φ inductively, as follows: The satisfaction relation for the equality atoms t ≈ u and the Boolean connectives ∧, ¬ are the classical ones from first-order logic. The (SL, T )-satisfiability problem asks whether there is a T -model I such that (I, h) | = SL for some heap h.
In this paper we tackle the (SL, T )-satisfiability problem, under the assumption that the quantifier-free data theory T = (Σ, I) has a decidable satisfiability problem for constraints involving Σ-terms. It has been proved [9] that the satisfiability problem is PSPACE-complete for the fragment of separation logic in which Data = Loc × Loc.
Here we generalize this result to any combination of theories whose satisfiability, for the quantifier-free fragment, is in PSPACE. This is, in general, the case of most SMT theories, which are typically in NP, such as the linear arithmetic of integers and reals, possibly with sets and uninterpreted functions, etc.

Reducing SL (T ) to Multisorted Second-Order Logic
It is well-known [21] that separation logic cannot be formalized as a classical (unsorted) first-order theory, for instance, due to the behavior of the * connective, that does not comply with the standard rules of contraction φ ⇒ φ * φ and weakening φ * ϕ ⇒ φ 5 . The basic reason is that φ * ϕ requires that φ and ϕ hold on disjoint heaps. Analogously, φ ⊸ ϕ holds on a heap whose extensions, by disjoint heaps satisfying φ, must satisfy ϕ. In the following, we leverage from the expressivity of multi-sorted first-order theories and translate SL(T ) formulae into quantified formulae in the language of T , assuming that T subsumes a theory of sets and uninterpreted functions.
The integration of separation logic within the DPLL(T) framework [12] requires the input logic to be presented as a multi-sorted logic. To this end, we assume, without loss of generality, the existence of a fixed theory T = (Σ, I) that subsumes a theory of sets Set(σ) [1], for any sort σ of set elements, whose functions are the union ∪, intersection ∩ of sort Set(σ) × Set(σ) → Set(σ), singleton {.} of sort σ → Set(σ) and emptyset ∅ of sort Set(σ). We write ℓ ⊆ ℓ ′ as a shorthand for ℓ ∪ ℓ ′ ≈ ℓ ′ and t ∈ ℓ for {t} ⊆ ℓ, for any terms ℓ and ℓ ′ of sort Set(σ) and t of sort σ. The interpretation of the functions in the set theory is the classical (boolean) one.
Also, we assume without loss of generality the existence of infinitely many function symbols pt, pt ′ , . . . ∈ Σ of sort Loc → Data, where Loc and Data are two fixed sorts of T , such that for any interpretation I ∈ I, Loc I is an infinite countable set 6 . We do not assume any particular interpretation of these symbols in the following and treat them as uninterpreted function symbols.
The main idea is to express the atoms and connectives of separation logic in multisorted second-order logic by means of a transformation, called labeling, which introduces (i) constraints over variables of sort Set(Loc) and (ii) terms over uninterpreted points-to functions of sort Loc → Data. We describe the labeling transformation using judgements of the form φ⊳[ℓ, pt], where φ is a SL(T ) formula, ℓ = ℓ 1 , . . . , ℓ n is a tuple of variables of sort Set(Loc) and pt = pt 1 , . . . , pt n is a tuple of uninterpreted function symbols occurring under the scopes of universal quantifiers. To ease the notation, we write ℓ and pt instead of the singleton tuples ℓ and pt . In the following, we also write ℓ for Intuitively, a labeled formula φ ⊳[ℓ, pt] says that it is possible to build, from any of its satisfying interpretations I, a heap h such that . More precisely, a variable ℓ i defines a slice of the domain of the (global) heap, whereas the restriction of pt i to (the interpretation of) ℓ i describes the heap relation on that slice. Observe that each interpretation of ℓ and pt, such that ℓ I i ∩ ℓ I j = ∅, for all i j, defines a unique heap. First, we translate an input SL(T ) formula φ into a labeled second-order formula, with quantifiers over sets and uninterpreted functions, defined by the rewriting rules in Figure 1. A labeling step φ[ϕ] =⇒ φ[ψ/ϕ] applies if ϕ and ψ match the antecedent and consequent of one of the rules in Figure 1, respectively. It is not hard to show that this rewriting system is confluent, and we denote by φ⇓ the normal form of φ with respect to the application of labeling steps.
The reduction to second-order logic is given below: The following lemma reduces the (SL, T )-satisfiability problem to the satisfiability of a quantified fragment of the multi-sorted second-order theory T , that contains sets and uninterpreted functions. For an interpretation I, a variable x and a value s ∈ σ I x , we denote by I[x ← s] the extension of I which maps x into s and behaves like I for all other symbols. We extend this notation to tuples x = x 1 , . . . , x n and s = s 1 , . . ., s n and write

Lemma 1.
Given a SL(T ) formula ϕ and tuples ℓ = ℓ 1 , . . . , ℓ n and pt = pt 1 , . . . , pt n for n > 0, for any interpretation I of T and any heap h: Although, in principle, satisfiability is undecidable in the presence of quantifiers and uninterpreted functions, the result of the next section strenghtens this reduction, by adapting the labeling rules for * and ⊸ ( Figure 1) to use bounded quantification over finite (set) domains.

A Reduction of SL (T ) to Quantifiers Over Bounded Sets
In the previous section, we have reduced any instance of the (SL, T )-satisfiability problem to an instance of the T -satisfiability problem in the second-order multi-sorted theory T which subsumes the theory Set(Loc) and contains several quantified uninterpreted function symbols of sort Loc → Data. A crucial point in the translation is that the only quantifiers occurring in T are of the forms ∀ℓ and ∀pt, where ℓ is a variable of sort Set(Loc) and pt is a function symbol of sort Loc → Data. Leveraging from a small model property for SL over the data domain Data = Loc × Loc [9], we show that it is sufficient to consider only the case when the quantified variables range over a bounded domain of sets. In principle, this allows us to eliminate the universal quantifiers by replacing them with finite conjunctions and obtain a decidability result based on the fact that the quantifier-free theory T with sets and uninterpreted functions is decidable. Since the cost of a-priori quantifier elimination is, in general, prohibitive, in the next section we develop an efficient lazy quantifier instantiation procedure, based on counterexample-driven refinement. For reasons of self-containment, we quote the following lemma [23] and stress the fact that its proof is oblivious of the assumption Data = Loc× Loc on the range of heaps. Given a formula φ in the language SL(T ), we first define the following measure: The small model property is given by the next lemma: Based on the fact that the proof of Lemma 2 [23] does not involve reasoning about data values, other than equality checking, we refine our reduction from the previous section, by bounding the quantifiers to finite sets of constants of known size. To this end, we assume the existence of a total order on the (countable) set of constants in Σ of sort Loc, disjoint from any Σ-terms that occur in a given formula φ, and define Bnd(φ,C) = {c m+1 , . . . , c m+|φ| }, where m = max{i | c i ∈ C}, and m = 0 if C = ∅. Clearly, we have Pt(φ) ∩ Bnd(φ,C) = ∅ and also C ∩ Bnd(φ,C) = ∅, for any C and any φ.
Observe that the result of the labeling process is a formula in which all quantifiers are of the form ∀ℓ 1 where L i 's and D i 's are finite sets of terms, none of which involves quantified variables, and ψ is a formula in the theory T with sets and uninterpreted functions. Moreover, the labeling rule for φ ⊸ ψ ⊳ [ℓ, pt,C] uses a fresh constant d that does not occur in φ or ψ.

A Counterexample-Guided Approach for Solving SL (T ) Inputs
This section presents a novel decision procedure for the (SL, T )-satisfiability of the set of quantifier-free SL (T ) formulae ϕ. To this end, we present an efficient decision procedure for the T -satisfiability of (ϕ ⊳ [ℓ, pt,C])⇓, obtained as the result of the transformation described in Section 4. The main challenge in doing so is treating the universal quantification occurring in (ϕ ⊳ [ℓ, pt,C])⇓. As mentioned, the key to decidability is that all quantified formulae in (ϕ ⊳ [ℓ, pt,C])⇓ are equivalent to formulas of the form ∀x.( x ⊆ s) ⇒ ϕ, where each term in the tuple s is a finite set (or product of sets) of ground Σ-terms. For brevity, we write ∀x ⊆ s.ϕ to denote a quantified formula of this form. While such formulae are clearly equivalent to a finite conjunction of instances, the cost of constructing these instances is in practice prohibitively expensive. Following recent approaches for handling universal quantification [13,19,6,20], we use a counterexample-guided approach for choosing instances of quantified formulae that are relevant to the satisfiability of our input. The approach is based on an iterative procedure maintaining an evolving set of quantifier-free Σ-formulae Γ, which is initially a set of formulae obtained from ϕ by a purification step, described next. We associate each closed quantified formula a boolean variable A, called the guard of ∀x.ϕ, and a (unique) set of Skolem symbols k of the same sort as x. We write (A, k) ⇌ solve SL(T) (ϕ): Let C be a set of fresh constants of sort Loc such that | |C| | = |ϕ|. Let ℓ and pt be a fresh symbols of sort Set(Loc) and Loc ⇒ Data respectively. Return solve T (⌊(ϕ ⊳ [ℓ, pt,C])⇓⌋ * ).
solve T (Γ): where (A, k) ⇌ ∀x ⊆ s.ψ. 3. Let t be a vector of terms, such that t ⊆ s, and t J = k J .
Return ∀x.ϕ to denote that A and k are associated with ∀x.ϕ. For a set of formulae Γ, we write Q(Γ) to denote the set of quantified formulae whose guard occurs within a formula in Γ. We write ⌊ψ⌋ for the result of replacing in ψ all closed quantified formulae (not occurring beneath other quantifiers in ψ) with their corresponding guards. Conversely, we write ⌈Γ⌉ to denote the result of replacing all guards in Γ by the quantified formulae they are associated with. We write ⌊ψ⌋ * denote the (smallest) set of Σ-formulae where: It is easy to see that if ψ is a Σ-formula possibly containing quantifiers, then ⌊ψ⌋ * is a set of quantifier-free Σ-formulae, and if all quantified formulas in ψ are of the form ∀x ⊆ s.ϕ mentioned above, then all quantified formulas in Q(⌊ψ⌋ * ) are also of this form.
Our algorithm solve SL(T) for determining the (SL, T )-satisfiability of input ϕ is given in Figure 3. It first constructs the set C based on the value of |ϕ|, which it computes by traversing the structure of ϕ. It then invokes the subprocedure solve T on the set ⌊(ϕ ⊳ [ℓ, pt,C])⇓⌋ * where ℓ and pt are fresh free symbols.
At a high level, the recursive procedure solve T takes as input a (quantifier-free) set of T -formulae Γ, where Γ is T -unsatisfiable if and only if (ϕ ⊳ [ℓ, pt,C])⇓ is. On each invocation, solve T will either(i) terminate with "unsat", in which case our input ϕ is T -unsatisfiable, (ii) terminate with "sat", in which case our input ϕ is T -satisfiable, or (iii) add the set corresponding to the purification of the instance ⌊A ⇒ ψ[t/x]⌋ * to Γ and repeats.
In more detail, in Step 1 of the procedure, we determine the T -satisfiability of Γ using a combination of a satisfiability solver and a decision procedure for T 8 . If Γ is T -unsatisfiable, since Γ is T -entailed by ⌈Γ⌉, we may terminate with "unsat". Otherwise, there is a T -model I for Γ and T . In Step 2 of the procedure, for each A that is interpreted to be true by I, we check whether Γ ∪ {A} T -entails ⌊ψ[k/x]⌋ for fresh free constants k, which can be accomplished by determining whether Γ ∪ {A, ¬⌊ψ[k/x]⌋} is T -unsatisfiable. If this check succeeds for a quantified formula ∀x.ψ, the algorithm has established that ∀x.ψ is entailed by Γ. If this check succeeds for all such quantified formulae, then Γ is equivalent to ⌈Γ⌉, and we may terminate with "sat". Otherwise, let Q + I (Γ) be the subset of Q(Γ) for which this check did not succeed. We call this the set of active quantified formulae for (I, Γ). We consider an active quantified formula that is minimal with respect to the relation ≺ Γ,I over Q(Γ), where: By this ordering, our approach considers innermost active quantified formulae first. Let ∀x.ψ be minimal with respect to ≺ Γ, Step 3 of the procedure, we choose a tuple of terms t = (t 1 , . . . , t n ) based on the model J, and add to Γ the set of formulae obtained by purifying A ⇒ ψ[t/x], where A is the guard of ∀x ⊆ s.ψ. Assume that s = (s 1 , . . . , s n ) and recall that each s i is a finite union of ground Σ-terms. We choose each t such that t i is a subset of s i for each i = 1, . . .n, and t J = k J . These two criteria are the key to the termination of the algorithm: the former ensures that only a finite number of possible instances can ever be added to Γ, and the latter ensures that we never add the same instance more than once.

Terminates.
By Theorem 1, solve SL(T) is a decision procedure for the (SL, T )-satisfiability of the language of quantifier-free SL (T ) formulae. The following corollary gives a tight complexity bound for the (SL, T )-satisfiability problem.

Corollary 1. The (SL, T )-satisfiability problem is PSPACE-complete for any theory T whose satisfiability (for the quantifier-free fragment) is in PSPACE.
In addition to being sound and complete, in practice, the approach solve SL(T) terminates in much less time that its theoretical worst-case complexity, given by the above corollary. This fact is corroborated by our evaluation of our prototype implementation of the algorithm, described in Section 6, and in the following examples.
Step 3 of the procedure recursively invokes solve T on Γ 1 , where: The set Γ 1 is T -unsatisfiable, since the added constraint contradicts A 4 ∧ y ≈ nil.

Integration in DPLL(T )
We have implemented the algorithm described in this section within the SMT solver CVC4 [3]. Our implementation accepts an extended syntax of SMT lib version 2 format [4] for specifying SL (T ) formulae. In contrast to the presentation so far, our implementation does not explicitly introduce quantifiers, and instead treats SL atoms natively using an integrated subsolver that expands the semantics of these atoms in lazy fashion. In more detail, given a SL (T ) input ϕ, our implementation lazily computes the expansion of (ϕ ⊳ [ℓ, pt,C])⇓ based on the translation rules in Figures 1 and 2 and the counterexample-guided instantiation procedure in Figure 3. This is accomplished by a module, which we refer to as the SL solver, that behaves analogously to a DPLL(T )style theory solver, that is, a dedicated solver specialized for the T -satisfiability of a conjunction of T -constraints 9 .
The DPLL(T ) solving architecture [12] used by most modern SMT solvers, given as input a set of quantifier-free T -formulae Γ, incrementally constructs of set of literals over the atoms of Γ until either it finds a set M that entail Γ at the propositional level, or determines that such a set cannot be found. In the former case, we refer to M as a satisfying assignment for Γ. If T is a combination of theories T 1 ∪ . . . ∪ T n , then M is partitioned into M 1 ∪ . . . ∪ M n where the atoms of M i are either T i -constraints or (dis)equalities shared over multiple theories. We use a theory solver (for T i ) to determine the T i -satisfiability of the set M i , interpreted as a conjunction. Given M i , the solver will either add additional formulae to Γ, or otherwise report that M i is T i -satisfiable.
For SL (T ) inputs, we extend our input syntax with a set of functions: →: Loc × Data → Bool * n : Bool n → Bool emp : Bool ⊸: Bool × Bool → Bool lbl : Bool × Set(Loc) → Bool which we call spatial functions 10 . We refer to lbl as the labeling predicate, which can be understood as a placeholder for the ⊳ transformation in Figures 1 and 2. We refer to p(t) as an unlabeled spatial atom if p is one of {emp, →, * n , ⊸} and t is a vector of terms not containing lbl. If a is an unlabeled spatial atom, We refer to lbl(a, ℓ) as a labeled spatial atom, and extend these terminologies to literals. We assume that all occurrences of spatial functions in our input ϕ occur only in unlabeled spatial atoms. Moreover, during execution, our implementation transforms all spatial atoms into a normal form, by applying associativity to flatten nested applications of * , and distributing Σ-formulae over spatial connectives, e.g.
When constructing satisfying assignments for ϕ, we relegate the set of all spatial literals M k to the SL solver. For all unlabeled spatial literals (¬)a, we add to Γ the formula (a ⇔ lbl(a, ℓ 0 )), where ℓ 0 is a distinguished free constant of sort Set(Loc). Henceforth, it suffices for the SL solver to only consider the labeled spatial literals in M k . To do so, firstly, it adds to Γ formulae based on the following criteria, which model one step of the reduction from Figure 1: where each ℓ i is a fresh free constant, and ϕ i [ℓ i ] denotes the result of replacing each spatial atom a in ϕ i with lbl(a, ℓ i ). These formulae are added eagerly when such literals are added to M k . To handle negated * -atoms and positive ⊸-atoms, the SL solver adds to Γ formulae based on the criteria: where each t i and f i is chosen based on the same criterion as described in Figure 3. For wand, we write CVC4 uses a scheme for incrementally checking the T -entailments required by solve T , as well as constructing models J satisfying the negated form of the literals in literals in M k before choosing such terms 11 . The formula of the above form are added to Γ lazily, that is, after all other solvers (for theories T i ) have determined their corresponding sets of literals M i are T i -satisfiable. Partial Support for Quantifiers In many practical cases it is useful to check the validity of entailments between existentially quantified SL(T ) formulae such as ∃x . φ(x) and ∃y . ψ(y). Typically, this problem translates into a satisfiability query for an SL(T ) formula ∃x∀y . φ(x) ∧ ¬ψ(y), with one quantifier alternation. A partial solution to this problem is to first check the satisfiability of φ. If φ is not satisfiable, the entailment holds trivially, so let us assume that φ has a model. Second, we check satisfiability of φ ∧ ψ. Again, if this is unsatisfiable, then the entailment cannot hold, because there exists a model of φ which is not a model of ψ. Else, if φ ∧ ψ has a model, we add an equality x = y for each pair of variables (x, y) ∈ x × y that are mapped to the same term in this model, the result being a conjunction E(x, y) of equalities. Finally, we check the satisfiability of the formula φ ∧ ¬ψ ∧ E. If this formula is unsatisfiable, the entailment is valid, otherwise, the test is inconclusive.

Evaluation
We tested our implementation of the (SL, T )-satisfiability procedure in CVC4 (version 1.5 prerelease) on two kinds of benchmarks: (i) finite unfoldings of inductive predicates with data constraints, mostly inspired by existing benchmarks, such as SL-COMP'14 [?], and (ii) verification conditions automatically generated by applying the weakest precondition calculus of [15] to the program loops in Figure 4 several times. All experiments were run on a 2.80GHz Intel(R) Core(TM) i7 CPU machine with with 8MB of cache 12 . For a majority of benchmarks, the runtime of CVC4 is quite low, with the exception of the n = 4, 8 cases of the entailments between tree n 1 and tree n 2 formulae, which resulted in a timeout after 300 seconds. 1: while w nil do 2: assert(w.data = 0) 3: v := w; 4: w := w.next; 5: dispose(v); 6: do (z)disp 1: while u nil do 2: assert(u.data = 0) 3: w := u.next; 4: u.next := v; 5: v := u; 6: u := w; lseg 2 (x,y,a) emp∧x=y∨∃z∃b . unsat unsat unsat unsat unsat x →(a,z) * lseg 1 (z,y,b)∧b=a+10 x →(a,z) * lseg 2 (z,y,b)∧a≤b < 0.01s < 0.01s < 0.01s 0.01s 0.01s tree 1 (x,a) emp∧x=nil∨∃y∃z∃b∃c . tree 2 (x,a) emp∧x=nil∨∃y∃z∃b∃c . unsat unsat unsat timeout timeout x →(a,y,z) * tree 1 (y,b) * tree 1 (z,c)∧ x →(a,y,z) * tree 2 (y,b) * tree 2 (z,c)∧ < 0.01s 0.06s 1.89s > 300s > 300s b=a−10∧c=a+10 b≤a∧a≤c unsat unsat unsat unsat unsat x →a * pos 1 (y,b) x →a * neg 1 (y,b) 0.02s 0.04s 0.11s 0.25 s 3.01s  The first set of experiments is reported in Table 1. We have considered the following inductive predicates commonly used as verification benchmarks [?]. Here we check the validity of the entailment between lhs and rhs, where both predicates are unfolded n = 1, 2, 3, 4, 8 times. The second set of experiments, reported in Table 1, considers the verification conditions of the forms ϕ ⇒ wp(l, φ) and ϕ ⇒ wp n (l, φ), where wp(l, φ) denotes the weakest precondition of the SL formula φ with respect to the sequence of statements l, and wp n (l, φ) = wp(l, . . . wp(l, wp(l, φ)) . . .) denotes the iterative application of the weakest precondition n times in a row. We consider the loops depicted in Figure 4, where, for each loop l we consider the variant zl as well, which tests that the data values contained within the memory cells are 0, by the assertions on line 2. The postconditions are specified by finite unfoldings of the inductive predicates ls and zls (Figure 4).

Conclusions
We have presented a decision procedure for quantifier-free SL (T ) formulas that relies on a efficient, counterexample-guided approach for establishing the T -satisfiability of formulas having quantification over bounded sets. We have described an implementation of the approach as an integrated subsolver in the DPLL(T )-based SMT solver CVC4, showing the potential of the procedure as a backend for tools reasoning about low-level pointer and data manipulations. For future work, we would like to extend the approach to be applicable to cases where Loc may have a finite interpretation, and improve the heuristics used by our decision procedure for choosing quantifier instantiations, in particular for cases with many quantifier alternations.  (1) and (2), we easily obtain that (2). "⇐ Let h and h ′ be tuples of heaps satisfying conditions (1) and (2) The proof is by induction on the structure of ϕ, among the lines of the proof of Lemma 1. In particular, it can be easily verified that the quantified sets variables and uninterpreted functions belong to the domains required by the rules of Figure 2.  Proof. Assume solve T (Γ i ) calls solve T (Γ i+1 ) for i = 0, . . . , n − 1, where n is finite and Γ 0 = ⌊ψ⌋ * . By definition of solve T and Lemma 4 (2), it can be shown that ⌈Γ i ⌉ and ⌈Γ i+1 ⌉ are equisatisfiable in T , and thus by induction ⌈Γ j ⌉ and ⌈Γ k ⌉ are equisatisfiable in T for each j, k ∈ {1, . . ., n}.
To show Part (2), without loss of generality, solve T (Γ n ) answers "sat". Then Γ n is T -satisfiable with model I. We argue that I satisfies ⌈Γ n ⌉, which implies that ⌈Γ 0 ⌉ is T -satisfiable, and thus by Lemma 4.2, ψ is T -satisfiable. Assume that I satisfies Γ n but does not satisfy ⌈Γ n ⌉. Thus, A I (∀x.ψ) I for some ∀x.ψ ∈ Q(Γ n ) where (A, k) ⇌ ∀x.ψ. In the case that A I = ⊥ and (∀x.ψ) I = ⊤, note that I does not satisfy the formula (¬A ⇒ ⌊¬ϕ[k/x]⌋) ∈ Γ n . In the case that A I = ⊤ and (∀x.ψ) I = ⊥, by the definition of solve T , we have Γ n , A | = T ⌊ψ[k/x]⌋. By Lemma 5, we have that Γ n | = T ∀x.ψ. Since I is a model of Γ n , it must be the case that (∀x.ψ) I = ⊤, contradicting the assumption that (∀x.ψ) I = ⊥. This contradicts the assumption that I does not satisfy ⌈Γ n ⌉.
To show Part (3), first note that the checks for T -satisfiability and T -entailment terminate, by assumption of a decision procedure for the T -satisfiability of quantifierfree formulae. Moreover, for each quantified formula ∀x.ψ, only a finite number of instances A ⇒ ψ[t/x] exist for which the algorithm will add ⌊A ⇒ ψ[t/x]⌋ * to Γ, which implies that the algorithm will consider only a finite number of quantified formulae, each for which only a finite number of instances will be added in this way. Thus, it suffices to show that the algorithm adds to Γ only sets ⌊A ⇒ ψ[t/x]⌋ * that are not a subset of Γ. Assume this is not the case for some ⌊A ⇒ ψ[t/x]⌋ * , where ∀x.ψ ∈ Q(Γ n ), ∀x.ψ is ≺ Γ,I -minimal, and (A, k) ⇌ ∀x.ψ. The terms t meet the criteria in the procedure, in particular, for some model Proof. PSPACE-hardness is by the reduction from QSAT, which generalizes [9, Definition 7] to our case. Let φ ≡ ∀x 1 ∃y 1 . . . ∀x n ∃y n . ψ be an instance of QSAT, where ψ is a boolean combination of the variables x i and y i of sort Bool. We encode φ in SL(T ) using the translation function Tr(.), defined by induction on the structure of φ: To prove that (SL, T )-satisfiability is in PSPACE, we analyse the space complexity of the solve SL(T) algorithm. First, for any SL(T )-formula ϕ, let Size(ϕ) be the size of the syntax tree of ϕ. Clearly | |⌊ϕ⌋ * | | ≤ Size(ϕ), and moreover, Size(ψ) ≤ Size(ϕ) for each


extfieldsofstudy:
Physics
Computer Science

text:
New Embedded Denotes Fuzzy C-Mean Application for Breast Cancer Density Segmentation in Digital Mammograms

In this research we explore the application of normalize denoted new techniques in advance fast c-mean in to the problem of finding the segment of different breast tissue regions in mammograms. The goal of the segmentation algorithm is to see if new denotes fuzzy c- mean algorithm could separate different densities for the different breast patterns. The new density segmentation is applied with multi-selection of seeds label to provide the hard constraint, whereas the seeds labels are selected based on user defined. New denotes fuzzy c- mean have been explored on images of various imaging modalities but not on huge format digital mammograms just yet. Therefore, this project is mainly focused on using normalize denoted new techniques employed in fuzzy c-mean to perform segmentation to increase visibility of different breast densities in mammography images. Segmentation of the mammogram into different mammographic densities is useful for risk assessment and quantitative evaluation of density changes. Our proposed methodology for the segmentation of mammograms on the basis of their region into different densities based categories has been tested on MIAS database and Trueta Database.

Introduction
Cancer is the leading cause of death in humans. One of the causes of death was cancer breast cancer. Breast cancer is cancer that occurs in the breast due to uncontrolled growth of cells of glands and ducts, thus damaging surrounding organs or tissues and spread to other body gets. To help the radiology and radiologist doctor expert in detecting cancer, patients can perform mammography. Mammography is an examination using X-rays to provide a picture of soft tissues in the breast. In the field of medicine, radiologists often have difficulty in observing the raw image of mammography, because the image produced has a degree of gray so it is difficult to see clear recognition of the cancer area. To overcome this necessary image processing operations one such image processing segmentation. Mammography image segmentation is a process to clarify and sharpen up the image of a feature or features segmented by division Cluster.
Breasts have a complex structure and compact with glands, and fat layer is thick and fibrous tissues affected by changes in female hormones estrogen and progesterone. Challenges in the compact segment image which is to be preferred, time-consuming and rather subjective. Development approach for segmenting each pixel in a cluster of its own into the impact of the information clear spatial give it a good medium for the interpreting prevail. The study found that the potential possibility of automatic algorithm to segmentation breast density in the evolution of longitudinal studies. A longitudinal study showed segmentation trend decline in the ratio depends on the number of early breast density.
Mammography containing quantities pixel density has been found to be a strong risk factor for breast cancer. Helping with spatial data available in highlight form and structure of the cancer helps doctors to interpret. A method of storing, accessing, organizing, and comparing spatial data spatial invitation to override data to support the process of analysis takes a too long time to process. This method is based on the classification of pixels in which a different approach known in the literature for breast density segments are integrated and expanded. In addition, the method that combines knowledge of trained observers, using segmentation obtained by user-assisted Fuzzy C-Mean (FCM) as training data. Remarkable novel ingredient (matrix normalization) purr into the FCM algorithm to enhance their routine (denote) whilst increase speed. This approach straightforward absorb in highly flexible fine-grained parallelism computing model.
Digital mammography nowadays generated in the database already been digitized to the edge pixel 50 micron scan microdensitometer Joyce-Loebl, linear devices in optical density range 0 -3.2 and represent each pixel with 8-bit. Although the database is so great detail still cannot help personalize medical radiologist to interpret early breast cancer properly

Classification of the breast according density
In clinical practice regularly check your breasts through breast self examination did not identifying the density of the mammary gland because does not felt. X-ray is a test used to detect changes in the breast tissue to penetrate various types of breast tissue relative to the amount of fat, connective tissue and epithelial to determine the radiographic appearance of the breast on a mammogram. Light (not radiolucent) areas on a mammogram representing fibrous and glandular tissue in the breast, while, dark (radiolucent) mostly fat regions [1], [2]. The difference density pattern classification methods are needed, Wolfe classification has been traditionally used in clinical practice and research. classification has four patterns of breast parenchyma or six category classification system based on a visual estimate of the density per cent. Breast imaging reporting and data system (BIRADS) classification. The density of the four categories are: BIRADS-1 shows the breast, especially fat; BIRADS-2 density scattered fibro-glandular; BIRADS-3 breast heterogeneous solid and BIRADS-4, the highest level, which is very dense breasts that can obscure the wound [3], [2]. Examples of the types of breast are shown in Figure 1.
Other measure that is related with density is sensitivity, because with high mammographic density have a reduced ability of detecting an existing cancer. It is very difficult locate ill-defined cancers within an opaque uniform background. Thus, as mammographic breast density is a strong predictor of breast cancer the first step of image and processing analysis of mammogram is the density classification. In first two stage BI-RADS 1 and 2, the accumulation of cancer is unexpected and need screening to identify density uprising. Here focused research to improve quantification of medical practice for formation and existence of abnormality.

Lesion Detection
There are a number of lesions that can be present in a breast. Develop algorithms that detection microcalcifications and masses, the two most common abnormalities in breast cancer. The detection of masses can be divided in two main blocks, the detection of suspicious regions and a posterior step of classification of those regions, which is typically called false positive reduction.

Micro-Calcifications Detection
Breast calcifications are deposits of calcium inside breast tissue. They appear widespread in the breast and most women will have a few on their mammograms at some point in time. Most calcifications will not be detected during clinical exams or breast self-examination. However, mammography allows to find them long prior to they could move forward into an actual lump. This fact helps explaining why developed countries are adopting the so-called screening programs, which mainly consist in promoting regular women examinations using mammography.

Figure 2. Micro-Calcifications Detection
Develop a new approach for the detection of micro-calcifications and clusters. The individual microcalcification detection is based on learning the variation in morphology of the micro-calcifications using local image features. Afterwards, this set of features is used to train a pixel-based boosting classifier which at each round automatically selects the most salient micro-calcification feature. Therefore, when a new mammogram is tested, only the salient features are computed and used to classify each pixel of the mammogram as being part of a micro-calcification or actually being normal tissue as show in Figure 2. Afterwards, the micro-calcification clusters are found by inspecting the local neighbourhood of each micro-calcification.
Develop a new approach for the detection of micro-calcifications and clusters. The individual microcalcification detection is based on learning the variation in morphology of the micro-calcifications using local image features. Afterwards, this set of features is used to train a pixel-based boosting classifier which at each round automatically selects the most salient micro-calcification feature. Therefore, when a new mammogram is tested, only the salient features are computed and used to classify each pixel of the mammogram as being part of a micro-calcification or actually being normal tissue as show in Figure 2. Afterwards, the micro-calcification clusters are found by inspecting the local neighbourhood of each micro-calcification:

Fuzzy C-Mean With Normalize Denotes Approach
To an image with size, the supposition is as follows: is the gray level of the image; H(l) means the onedimensional gray statistic mapping function of the image. Namely, the definition is: If the above narration objective function follow our work in [4] is minimized, then the new F-FCM iteration functions are obtained.
Obviously, the speed of the F-FCM algorithm is enhanced greatly, and the result of sort is same with the FCM algorithm. Based on Equation (1), we proposed architecture implemented in a circuit fashion.

Software Interface Between LabVIEW and FPGA's
The goal of clustering is to partition data samples into different classes according to the samples' mutual similarity. First, a distance metric is defined to measure similarity. Next, by minimizing the overall cost, you can determine the centroids and partition scheme. This process is often iterative and the cluster centroids will converge after several iterations. Possible applications of clustering include pattern recognition, data mapping, image segmentation, and clustering.
Structures with multiple sub-diagrams, such as Case structures and Flat Sequence structures, have a separate VHDL entity for each case or frame as shown in Figure 3. These VHDL entities have names ending with diagram to indicate that they represent a sub-diagram. Re-entrant subVIs appears in the VHDL code in the same manner as structures appear. Re-entrant subVIs has multiple instances in the VHDL code hierarchy. These instances correspond to calls to the subVIs from the block diagram. Non-re-entrant subVIs includes special VHDL logic to manage the data flow to and from re-entrant subVIs.
For sake of brevity, the images considered in this section are gray-level images. Each data point xk represents a pixel with gray level values in the range between 0 and 255. For colour images, each pixel xk becomes a vector consisting of three colour components: red, green and blue. In the proposed architecture, each data point xk can be a scalar or a vector. Therefore, the proposed architecture can be directly applied to colour image segmentation by implementing xk as a 3-dimension vector. The performance of the image segmentation is measured by segmentation error rate, which intensity information using structural similarity index measure (SSIM) and Peak signal to noise ratio (PSNR). Experiment data segmentation error rate still ongoing.
The choice was made to use an FPGA, not only for its speed advantages but also for the ability to create functional logic blocks. This allowed many areas of the controller to function independently, without requiring complex threading or interrupts on the micro-controller. FPGAs can support large internal shift registers, which is important as thousands of bits need to be shifted out at a rapid rate. Figure 4 show Hardware / Software Code-sign Platform.  Designing the visual composition and temporal behaviour of a GUI is an important part of software application programming in the area of human-computer interaction. Its goal is to enhance the efficiency and ease of use for the underlying logical design of a stored program, a design discipline known as usability.
In this application graphical user interface or GUI is the type of interface that allows users to interact with electronic devices through graphical icons and visual indicators such as secondary notation use to employ number of cluster, as opposed to text-based interfaces, typed command labels whereby use to select mammogram image or text navigation. GUIs were introduced in reaction to the perceived steep learning curve of command-line interfaces which require commands to be typed on the keyboard. Meanwhile, the mammogram image applied and clustered result shown in window display panel 540 x 540 sizes as initial visual template, conclusive big data image (1024 x 1024) can be retrieved from designated folder database. All reconstructed image accumulated for medical image standard diagnosis. Images containing suspicious areas have associated pixel-level "ground truth" information about the locations and types of suspicious regions. Finally, execution time displayer window put on place for performance and evaluation purpose.

Experimental and Result
The medical image segmentation is implementing using FCM whilst objective test means is produced. Objective test is the repetition of a unit amount that maintains its size, within an allowable range of error, no matter which instrument, intended to measure the variable of interest, is used and no matter who or what relevant person or mammogram is measured. Both quantitative and qualitative characterization digital image in this research bonded on objective test. Illustration on Figure 6 indicates quantitative-(objective test) analysis of task for test meanwhile qualitative-(objective test) trend in test is the research outline.
Subjective test is a form of expression in the form of image to test medical personal knowledge, experience, skills and levels of cognitive abilities of personal by the response. They require medical personal to create their own responses, rather than selecting a response from a list of options. The objective measurements are an evaluation of detector performance alone, while the observer threshold contrast results include effects of observer detects ability, observer visual response, display magnification and processing, ambient viewing conditions including display reflection and scattered radiation and grid performance [5].
The objective analysis began with the generation of variance images from flat field images. These images were useful in obtaining a visual impression of the variance across the entire process of calcification [6]. Eventually, hope to perform objective test of the mammogram using measured image pixel data process automatically segmentation to identify regions of interest. The accuracy of Fuzzy C-Mean (FCM) is due to the employment of fuzziness for the clustering of each image pixel.
Propose of finding cluster centres by iteratively adjusting their position and minimizing an objective function. This approach to testing image processing remains objective. It is proven objective test using FCM approach for diagnostic purposes namely in assisting radiologist in interpreting the mammogram that they have to scrutinize. In this research objective test more suitable with proper process and method. Subjective test more manually depend on human experience (medical specialists). Factor influence depend on age, high, eye side vision and experience.

Qualitative Experiment and Result
In order to show the benefits of this research approach, a qualitative analysis is performed using the entire MIAS database (322 images in total) using previous researcher breast density segmentation (thresholding approaches). Figure 7 shows the results obtained for the MIAS database when using both excess entropy thresholding in [7] and the second one based on the multiclass Fuzzy C-Means clustering algorithm in [8] approaches for breast density quantification. Note that the performance of both algorithms for class BIRADS I is not the expected one, obtaining a large dispersion in the dense percentage ratio. The reason for this behaviour is that there is a set of mammograms correctly segmented (without dense cluster or being small), while there is another set incorrectly segmented.

Figure7.
Boxplot of breast dense percentage using the MIAS database and two well-known thresholding approaches. First row shows the results using the excess entropy thresholding, while second one using the multiclass Fuzzy C-Means clustering algorithm.
In these cases, the thresholding approaches segmented the outer part of the breast from the inner part due to the fact that pixels near the skin-line (those with less breast tissue) are darker than the other ones. Hence, in homogeneous fatty mammograms, this tends to produce an incorrect estimation of the threshold. In contrast, the rest of BIRADS classes show more compact results, increasing the median of the class according to the increasing density. This approach is based on the conjecture that the optimal thresholding corresponds to the segmentation with maximum structure. Introduce the excess entropy as a measure of the spatial structure of an image. There an adaptive thresholding method based on the maximization of excess entropy. It also use of uniformly distributed random lines to overcome the main drawbacks of the excess entropy computation. Performance of the segmentation bulky spatial in such a way but surface structure not allocated.
The fully-automated algorithm (multiclass Fuzzy C-Means clustering) was successful in identifying the fibroglandular tissue of the breast in digital mammographic images. These findings indicate that the proposed algorithm can provide some clinically relevant information from digital mammography for the assessment of breast density.
One surprising result was the relatively poor performance of the multiclass Fuzzy C-Means paradigm, previously used for density assessment in digitized film mammograms, in identifying the dense tissue region. Although BIRADS classification and quantification has often been the primary focus [10], this finding is in apparent contrast to findings by [7], who reported good visual agreement between FCM and expert markings [9]. Further investigation showed that one possible explanation for the poor performance of the 2-class FCM algorithm is the fact that majority gray-level intensity profiles of breast tissue as extracted from digital mammograms tend to be multi-modal, such as in the BIRADS-IV case illustrated in Figure 4. Given that appropriate selection of the number of clusters, k, is critical for proper clustering, the intensity profile of digital mammograms are complex enough that multi-class techniques, such as the one described in this work, may be required to appropriately analyze digital mammography images.
As breast tissue seen mammographically is a 2D superimposition of different tissue types with different image properties, future studies should seek to expand density based risk-stratification analysis beyond the dichotomous, fatty vs. dense tissue paradigm. Furthermore, as mammography is essentially limited by the effect of projection/ tissue superimposition, volumetric analysis of fibroglandular tissue through emerging tomography breast imaging modalities, such as breast tomosynthesis and magnetic resonance imaging, has been suggested as necessary to advance breast cancer risk modeling [10] and the approach described in this work could become the foundation for fully-automated density quantification from three-dimensional images.

Qualitative Performance and Evaluation Breast Density Segmentation (F-FCM) on MIAS
Database In order to show the benefits of our approach compared the obtained results with a new F-FCM method of normalized spatial density approach as mention in section 3.1 and 4.3.2. This new normalized with mapping and mesh technique portray aggregately to accelerate the matrix transform arithmetic and improve overall FCM algorithm to become F-FCM. The method is trained and tested using 322 digitized film mammographic images acquired with a variety of systems. A combination of segmentation strategies outperforms the application of single segmentation techniques. The value of ρ is set using data collected from experiment on mammogram digital images is set 0.0001. This is important for start performing experiment using ρ value setting for consistent application outcome result. The value of ρ is computed first time load mammogram image, there is possibility the value change as the source of mammogram came from different apparatus type.
A qualitative analysis is performed using MIAS database (322 images in total). Figure 8 show some selected MIAS image before and after segmentation whilst fatty and dense areas can clearly perceive. After segmenting the breast in both fatty and dense tissues, computed the percentage of segmented dense area relative to the overall breast area (fatty and dense areas). Afterwards, the constructed a boxplot analysis detailing this percentage according to each density class provided in the MIAS annotations (fatty, glandular and dense). This is shown in Figure 9. Observe that the percentage of dense area increases according to the class density. Note also that mammograms belonging to fatty class do almost not show any dense area, while dense mammograms have large percentage dispersion. Notice that a obtained several outliers in the fatty and glandular classes. This is due to the fact that there is a small set of mammograms brighter than the rest, and in this cases, the algorithm is not able to correctly recognize the fatty tissue. In these cases, a previous grey-level normalization of the image should be necessary. Figure 8 shows the mammogram samples of MIAS sample after applying our segmentation approach using our Fuzzy C-Mean (FCM) clustering. The lighter cluster shows the dense area, while the darker one shows the fatty tissue. Note that the dense area of the mammograms is segmented in a multiple and homogeneous region, except for the mammogram belonging to BIRADS I, BIRADS II, BIRADS III and BIRADS IV which has a small o bigger dense cluster. Moreover, observe that the size of the dense cluster increases as the density of the breast also increases. The performance of the presented algorithm is evaluated and shown it catch every micro-calcifications in form density mean. Repeated the same analysis but using the annotations provided by the radiologists, who classified the MIAS database according to the BIRADS standard. The results are shown in Figure 10. Note that the dense area of mammograms belonging to BIRADS I is significant increase, while mammograms belonging to BIRADS II have a small part of dense tissue. The dispersion in dense classes is now reduced, and the outliers have also been reduced. Moreover, according to the notches, the difference in the median of all classes is clearly significant.
However, comparing these results with those shown in Figure 7, the median is higher. This is also a consequence of bad threshold estimation. However, in this case, the bias is smaller due to the fact the tissue of the mammograms is more heterogeneous, and therefore, the estimated threshold is greater than the obtained when segmenting mammograms belonging to BIRADS I. The target intensity loosens whereby it over taken on pixel tabulated. Furthermore, structural dimension flatten on stand which not added value from previous medical machine CAD (DICOM) analysis.

Qualitative Performance and Evaluation Breast Density Segmentation (F-FCM) on Trueta Database
In this section, we repeat the same qualitative analysis but using the Trueta database and now analyzing 125 MLO (Mediolateral) and 125 CC (Craniocaudal) views independently. The preprocessing step of CC mammograms did not include the pectoral muscle removal since the muscle was not present in this view. Figure 11 shows the boxplots of the dense percentage obtained. The first row analyses the CC mammograms, while the second one analyses the MLO. Note that, in both cases, the percentage increases according to the BIRADS classes. However, we found two outliers using the CC set and two more when using the MLO. Note that the trend is similar when comparing both datasets, showing that our approach is able to correctly segment both MLO and CC mammograms. Comparing the obtained results using the MIAS and the ones using the Trueta database, we observe that the BIRADS I distribution is better defined when using the former database. This is due to the different nature of the databases. Remember that the MIAS is a digitized database, while the Trueta one is fully digital. In the Trueta database, almost all fatty mammograms have a small region segmented due to the fact that the digital database has more contrast than the digitized. Hence, some 13 ducts and linear structures that are brighter than the fatty breast tissue are incorrectly segmented. In contrast, the performance for the other classes is similar.
The approach was validated by comparing manual expert annotations with automatically obtained estimations. Transversal analysis of the breast density analysis of CC and MLO views of both breasts acquired in the same study showed a correlation coefficient of r = 0.96 between the mammographic density percentage for left and right breasts, whereas a comparison of both mammographic views showed a correlation of r = 0.95.

Conclusion
The performance of the initial pre-processing (thresholding approaches) step explained in "Initial Preprocessing Step", which was performed in order to remove background, annotations and pectoral muscle of the images briefly discussed. In general, the performance of these algorithms is good enough in most of the cases. However, for the MIAS database, there is a large set of images where the breast segmentation algorithm decreases its accuracy, incorrectly segmenting a small border of the breast. In contrast, regarding the Trueta database, the pectoral muscle is incorrectly segmented in few cases, having the problem of segmenting a small portion of fatty tissue besides the pectoral muscle. However, in both cases, the segmentation algorithm segments correctly the dense tissue due to the fact that the algorithm does not depend on the fatty tissue. Note that, for these special situations, as a small area of the fatty tissue has been suppressed, the ratio of dense area is slightly biased to higher values.
Compare between database --with the advent of confocal microscopy and other advanced imaging techniques--Furthermore, the spatial agreement between automated-algorithm segmentations and radiologic ground-truth (J=0.62±0.22) was found to be similar to the human-observer inter-reader variability of 0.65±0.18 previously reported by [11].
In F-FCM outcome, the classifications of cluster cover the spatial relationships within the cluster (i.e. between groups of micro-calcification that form a cluster). In additional, the F-FCM segmentation breast density highlighted the value of spatial aggregation into a level where densities mimic 3-D surface structure without brittle image structure (fringe 3-D image). Consensually, it helps medical prentices observe the structure also with other anatomical structures /tissue (i.e. linear structure, such as vessels and ducts). This contribution and expand the ontology especially their work on interpret micro-calcifications and masses. Strong agreement with radiologist-provided ground truth was obtained, both in terms of the quantitative estimate and the spatial agreement of the segmented dense tissue.