Annotation inference for separation logic based veri ers

Abstract. With the years, program complexity has increased dramati-cally: ensuring program correctness has become considerably more diffi-cult with the advent of multithreading, security has grown more promi-nent during the last decade, etc. As a result, static verification has be-come more important than ever. Automated verification tools exist, but they are only able to prove a limited set of properties, such as memory safety. If we want to prove full functional correctness of a program, other more powerful tools are avail-able, but they generally require a lot more input from the programmer: they often need the code to be verified to be heavily annotated. In this paper, we attempt to combine the best of both worlds by starting off with a manual verification tool based on separation logic for which we develop techniques to automatically generate part of the required anno-tations. This approach provides more flexibility: for instance, it makes it possible to automatically check as large a part of the program as possible for memory errors and then manually add extra annotations only to those parts of the code where automated tools failed and/or full correctness is actually needed.