@article{Lathouwers24,
title = {Survey of annotation generators for deductive verifiers},
journal = {Journal of Systems and Software},
volume = {211},
pages = {111972},
year = {2024},
issn = {0164-1212},
doi = {https://doi.org/10.1016/j.jss.2024.111972},
url = {https://www.sciencedirect.com/science/article/pii/S0164121224000153},
author = {Sophie Lathouwers and Marieke Huisman},
keywords = {Deductive verification, Specifications, Annotations, Specification inference, Specification generation, Survey},
abstract = {Deductive verifiers require intensive user interaction in the form of writing precise specifications, thereby limiting their use in practice. While many solutions have been proposed to generate specifications, their evaluations and comparisons to other tools are limited. As a result, it is unclear what the best approaches for specification inference are and how these impact the overall specification writing process. In this paper we take steps to address this problem by providing an overview of specification inference tools that can be used for deductive verification of Java programs. For each tool, we discuss its approach to specification inference and identify its advantages and disadvantages. Moreover, we identify the types of specifications that it infers and use this to estimate the impact of the tool on the overall specification writing process. Finally, we identify the ideal features of a specification generator and discuss important challenges for future research.}
}

{"_id":"RbNx5cnZt8LxiNd3x","bibbaseid":"lathouwers-huisman-surveyofannotationgeneratorsfordeductiveverifiers-2024","author_short":["Lathouwers, S.","Huisman, M."],"bibdata":{"bibtype":"article","type":"article","title":"Survey of annotation generators for deductive verifiers","journal":"Journal of Systems and Software","volume":"211","pages":"111972","year":"2024","issn":"0164-1212","doi":"https://doi.org/10.1016/j.jss.2024.111972","url":"https://www.sciencedirect.com/science/article/pii/S0164121224000153","author":[{"firstnames":["Sophie"],"propositions":[],"lastnames":["Lathouwers"],"suffixes":[]},{"firstnames":["Marieke"],"propositions":[],"lastnames":["Huisman"],"suffixes":[]}],"keywords":"Deductive verification, Specifications, Annotations, Specification inference, Specification generation, Survey","abstract":"Deductive verifiers require intensive user interaction in the form of writing precise specifications, thereby limiting their use in practice. While many solutions have been proposed to generate specifications, their evaluations and comparisons to other tools are limited. As a result, it is unclear what the best approaches for specification inference are and how these impact the overall specification writing process. In this paper we take steps to address this problem by providing an overview of specification inference tools that can be used for deductive verification of Java programs. For each tool, we discuss its approach to specification inference and identify its advantages and disadvantages. Moreover, we identify the types of specifications that it infers and use this to estimate the impact of the tool on the overall specification writing process. Finally, we identify the ideal features of a specification generator and discuss important challenges for future research.","bibtex":"@article{Lathouwers24,\ntitle = {Survey of annotation generators for deductive verifiers},\njournal = {Journal of Systems and Software},\nvolume = {211},\npages = {111972},\nyear = {2024},\nissn = {0164-1212},\ndoi = {https://doi.org/10.1016/j.jss.2024.111972},\nurl = {https://www.sciencedirect.com/science/article/pii/S0164121224000153},\nauthor = {Sophie Lathouwers and Marieke Huisman},\nkeywords = {Deductive verification, Specifications, Annotations, Specification inference, Specification generation, Survey},\nabstract = {Deductive verifiers require intensive user interaction in the form of writing precise specifications, thereby limiting their use in practice. While many solutions have been proposed to generate specifications, their evaluations and comparisons to other tools are limited. As a result, it is unclear what the best approaches for specification inference are and how these impact the overall specification writing process. In this paper we take steps to address this problem by providing an overview of specification inference tools that can be used for deductive verification of Java programs. For each tool, we discuss its approach to specification inference and identify its advantages and disadvantages. Moreover, we identify the types of specifications that it infers and use this to estimate the impact of the tool on the overall specification writing process. Finally, we identify the ideal features of a specification generator and discuss important challenges for future research.}\n}\n\n\n\n\n","author_short":["Lathouwers, S.","Huisman, M."],"key":"Lathouwers24","id":"Lathouwers24","bibbaseid":"lathouwers-huisman-surveyofannotationgeneratorsfordeductiveverifiers-2024","role":"author","urls":{"Paper":"https://www.sciencedirect.com/science/article/pii/S0164121224000153"},"keyword":["Deductive verification","Specifications","Annotations","Specification inference","Specification generation","Survey"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"article","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","dataSources":["cCvCnPTRQYq3qPe9y"],"keywords":["deductive verification","specifications","annotations","specification inference","specification generation","survey"],"search_terms":["survey","annotation","generators","deductive","verifiers","lathouwers","huisman"],"title":"Survey of annotation generators for deductive verifiers","year":2024}