Formal Techniques for Distributed Systems (FMOODS/FORTE 2011) vol:6722 pages:319-333
Lecture Notes in Computer Science
FMOODS/FORTE 2011 edition:13 location:Reykjavik, Iceland date:6-9 June 2011
With the years, program complexity has increased dramatically: ensuring program correctness has become considerably more difficult with the advent of multithreading, security has grown more prominent
during the last decade, etc. As a result, static verification has become 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 available,
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 annotations. 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.