Roberta Gori

Systematic Design of Separation Logics

Thanks to the locality principle, separation logics support modular, scalable analysis of large codebases by relying on local axioms and frame rules to focus only on the heap fragments required for verification. However, depending on the direction—forward vs. backward—and sense o...