I figure it can't hurt to also mention the Coq/software foundations style separation logic book. In it you build a sequential separation logic, and prove some

I figure it can't hurt to also mention the Coq/software foundations style separation logic book. In it you build a sequential separation logic, and prove some properties such as soundness (rather than a concurrent separation logic like e.g. Iris above). The related work section of the summary paper also has a rather extensive list of projects using separation logic, though i'll note I didn't see Infer [1], listed. [1]: https://www.chargueraud.org/teach/verif/ https://www.chargueraud.org/teach/verif/