Infer is the de-facto standard open-source static analysis framework built with separation logic at its core. Recently, Jules Villard and the Infer team at Meta developed the Pulse checker, which leverages incorrectness logic reasoning to guarantee (almost) no false positive bug finding. In this talk, we will put our security engineer’s hat and review software vulnerabilities which are currently out of reach for Infer, but are good candidates for automation. We will discuss a number of proposed improvements to increase Infer’s property coverage for security applications, and suggest implementation strategies among the different Infer modules to add these functionalities with minimal footprint.