Separation logic (SL) has gained widespread popularity as a formal foundation of tools that analyze and verify heap-manipulating programs. Its great asset lies in its assertion language, which can succinctly express how data structures are laid out in memory, and its discipline of local reasoning, which mimics human intuition about how to prove heap programs correct. This talk discusses approaches to automated reasoning in separation logics using SMT solvers. I will present fragments of SL that admit reductions to decidable first-order theories. I will also discuss incomplete approaches based on combinations of SL-style proof-theoretic reasoning and SMT techniques for some nonstandard models of SL. These techniques have been implemented in the deductive program verifier GRASShopper.