Paper Info
Title
Improving the usability of specification languages and methods for annotation-based verification
Abstract
It is widely recognized that human input is indispensable in deductive verification of real-world code. Verification engineers have to guide the proof search and provide information reflecting their insight into the workings of the program. Lately we have seen a shift towards an annotation-based paradigm --- sometimes called "verifying compiler" ---, where this information is provided in the form of program annotations instead of interactively during proof construction. Suspicions have been growing recently that expressing verification knowledge as annotations in their current form suffers from serious scalability and maintainability issues. In this paper, we pinpoint some of the biggest neuralgic spots and provide recommendations to the designers of annotation-based verification systems aimed to improve usability of specification languages and methods and, thus, the tool's productivity. We clarify the different purposes that annotations can serve and show why a certain class of annotations that are not program requirements is currently indispensable for proof construction. Moreover, we discuss how the use of data abstractions can be improved in annotation-based specifications.
Year
DOI
Venue
2010
10.1007/978-3-642-25271-6_4
FMCO
Keywords
Field
DocType
current form,proof search,deductive verification,specification language,verification knowledge,program requirement,verification engineer,annotation-based specification,annotation-based paradigm,annotation-based verification system,proof construction
Abstract data type,Proof search,Programming language,Annotation,Abstraction,Software engineering,Computer science,Usability,Compiler,Maintainability,Scalability
Conference
Citations 
PageRank 
References 
2
0.40
12
Authors
3
Name
Order
Citations
PageRank
Bernhard Beckert186286.50
Thorsten Bormer2584.90
Vladimir Klebanov320713.69