HIP/SLEEK is an automated program verification framework based on separation logic.