Stellis: A Strategy Language for Purifying Separation Logic Entailments

Zhiyi Wang, Xiwei Wu, Yi Fang +5

Automatically proving separation logic entailments is a fundamental challenge in verification. While rule-based methods rely on separation logic rules (lemmas) for automation, thes…