Output details

Loop invariant synthesis in a combined abstract domain

<07> Automated verification of memory safety and functional correctness for heap-manipulating programs is a challenging task. Existing verification systems rely heavily on user annotations to help guide the verification, which can be cumbersome, error-prone and can significantly restrict the usability of the verification. We propose a novel static analysis to automatically synthesise loop invariants. The work is original and significant as it is the first analysis developed over an abstract domain combined with both separation and numerical information, and it can discover non-trivial loop invariants that could not be inferred before. This work is an output of an EPSRC-funded project EP/G042322.