A recent (and in a lot of cases more useful) trend is showing that programs are incorrect (buggy) rather than correct.
Specifically, there is a recent an analogue of SL, called incorrectness separation logic (ISL) that i designed to prove the presence of bugs, i.e. detect bugs:
The main advantage of ISL is that it uses under-approximation, unlike original SL which uses over-approximation. That is to say, SL is used to show ALL program behaviours are correct, and in the process of doing so we may over-approximate the set of program behaviours. By contrast, ISL is used to show there are SOME incorrect (buggy) program behaviours.
ISL was implemented in a tool called PulseX at Facebook and shown to be a very scalable approach (comparable with and in some cases better than the state-of-the art Infer tool):
Specifically, there is a recent an analogue of SL, called incorrectness separation logic (ISL) that i designed to prove the presence of bugs, i.e. detect bugs:
https://link.springer.com/chapter/10.1007/978-3-030-53291-8_...
The main advantage of ISL is that it uses under-approximation, unlike original SL which uses over-approximation. That is to say, SL is used to show ALL program behaviours are correct, and in the process of doing so we may over-approximate the set of program behaviours. By contrast, ISL is used to show there are SOME incorrect (buggy) program behaviours.
ISL was implemented in a tool called PulseX at Facebook and shown to be a very scalable approach (comparable with and in some cases better than the state-of-the art Infer tool):
https://dl.acm.org/doi/abs/10.1145/3527325