Advancing Automated, Permission-Based Program Verification Using Symbolic Execution