We have recently published a paper in the 24th Static Analysis Symposium (SAS’17). The paper titled A Context-Sensitive Memory Model for Verification of C/C++ Programs describes a context-, field-, and array-sensitive pointer analysis for C and C++ programs. The slides used in the presentation can be found here.
The pointer analysis produces a finer-grained partition of memory so that SeaHorn can generate verification conditions involving complex low-level pointers and arrays constraints but yet they can be solved efficiently.
The code of the analysis is available in sea-dsa. sea-dsa is now the default pointer analysis used in SeaHorn, replacing the original llvm-dsa. Note that sea-dsa is a stand-alone project so you can use it in your analysis tool!