文章基本信息

标题：The Belgian Electronic Identity Card: a Verification Case Study
本地全文：下载
作者：Pieter Philippaerts ; Frédéric Vogels ; Jan Smans 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2011
卷号：46
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：In the field of annotation-based source code level program verification for Java-like languages, separation-logic based verifiers offer a promising alternative to classic JML based verifiers such as ESC/Java2, the Mobius tool or Spec#. Researchers have demonstrated the advantages of separation logic based verification by showing that it is feasible to verify very challenging (though very small) sample code, such as design patterns, or highly concurrent code. However, there is little experience in using this new breed of verifiers on real code. In this paper we report on our experience of verifying several thousands of lines of Java Card code using VeriFast, one of the state-of-the-art separation logic based verifiers. We quantify annotation overhead, verification performance, and impact on code quality (number of bugs found). Finally, our experiments suggest a number of potential improvements to the VeriFast tool.