Verifying C++ Dynamic Binding

06/03/2023
by   Niels Mommen, et al.
0

We propose an approach for modular verification of programs written in an object-oriented language where, like in C++, the same virtual method call is bound to different methods at different points during the construction or destruction of an object. Our separation logic combines Parkinson and Bierman's abstract predicate families with essentially explicitly tracking each subobject's vtable pointer. Our logic supports polymorphic destruction. Virtual inheritance is not yet supported. We formalised our approach and implemented it in our VeriFast tool for semi-automated modular formal verification of C++ programs.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset