Since 1960s, automated program verification has been considered as an extremely difficult topic in Computer Science, despite of the emergence of Floyd-Hoare logic. Since 1990s, with more efforts and resources devoted to this area, especially the contributions from industry communities including Microsoft Research and IBM Research Centre, there has been noticeable progress made in program verification early this century. Two typical examples include ASTRÉE, used to verify the absence of runtime errors in Airbus code, and SLAM, employed to verify protocol properties of procedural calls in device drivers by Microsoft. However, none of these tools considers heap. Specifically, ASTRÉE assumes no dynamic pointer allocation and no recursion, while SLAM assumes memory safety. Many important programs/systems that exist nowadays, such as Linux, Apache, and device drivers, all make frequent use of heap. Automated verification of heap-manipulating programs remains a very challenging topic. The emergence of separation logic in 2001-2002 has shed some light into this area. With the key idea of separation and the elegant frame rule, local reasoning can now be readily employed in program verification. Since 2004, there have been a large body of research work dedicated to automated program verification via separation logic, e.g. SpaceInvader/Abductor, Slayer, HIP/SLEEK, CSL etc. This paper offers a survey on a number of important research work along this line.