Title: Annotation inference for separation logic based verifiers
Authors: Vogels, Frédéric ×
Jacobs, Bart
Piessens, Frank
Smans, Jan #
Issue Date: 2011
Publisher: Springer
Host Document: Formal Techniques for Distributed Systems (FMOODS/FORTE 2011) vol:6722 pages:319-333
Series Title: Lecture Notes in Computer Science
Conference: FMOODS/FORTE 2011 edition:13 location:Reykjavik, Iceland date:6-9 June 2011
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.
ISBN: 978-3-642-21460-8
ISSN: 0302-9743
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
final.pdfPaper Published 94KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.