This paper presents a static analysis including a session-based type system using a Points-To analysis for verifying active object languages – object-oriented languages based on the actor paradigm with futures. We specify and verify not only interaction behaviors, but also constraints on object state and data expressed in a first-order formalization of heap memory. A Points-To analysis gives a lightweight analysis on dependency of constraints at different interactions, whose behaviors are checked by a session-based type system. Instead of specifying communication channels, we specify the interplay of futures and method calls on objects. We propose a session-based global specification and establish a local static verification framework to ensure the interacting objects will produce deadlock-free communication traces adhering to our specification.