Well I tasked myself with 6 days to implement this for a C program verifier.

https://arxiv.org/abs/1910.09521

Probably only going to manage one teeny component. But monadic second order logic, man.