Annotation Inference for Separation Logic Based Verifiers

Abstract : 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.
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01583323
Contributor : Hal Ifip <>
Submitted on : Thursday, September 7, 2017 - 11:10:23 AM
Last modification on : Thursday, February 21, 2019 - 10:31:47 AM

File

978-3-642-21461-5_21_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Frédéric Vogels, Bart Jacobs, Frank Piessens, Jan Smans. Annotation Inference for Separation Logic Based Verifiers. 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. pp.319-333, ⟨10.1007/978-3-642-21461-5_21⟩. ⟨hal-01583323⟩

Share

Metrics

Record views

49

Files downloads

141