Programs become more error-prone with inappropriate management of memory because of pointer aliasing, e.g., dereferencing null or dangling pointers, and memory leaks.PPTL^SL is a two-dimensional(spatial and temporal) logic which integrates separation logic with PPTL(propositional projection temporal logic).It is useful to describe and verify temporal properties of list manipulating programs.This paper first gives an overview of PPTL^SL, and then introduces the foundation of the tool SAT-PPTL^SL in detail.SAT-PPTL^SL can be used to check the satisfiability of PPTL^SL formulas according to the "isomorphic" relationship between PPTL^SL and PPTL.In addition, the paper presents examples to show the checking process of SAT-PPTL^SL and analyze the effect of some key parameters on the performance of SAT-PPTL^SL.