A Context-Sensitive Memory Model for Verification of C/C++ Programs
New paper in SAS'17

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!

*****
Written by SeaHorn on 01 October 2017