Approximate Verification in an Open Source World Articles uri icon

authors

  • PICKIN, SIMON JAMES
  • BREUER, PETER T.

publication date

  • April 2008

start page

  • 87

end page

  • 105

issue

  • 1

volume

  • 4

International Standard Serial Number (ISSN)

  • 1614-5046

Electronic International Standard Serial Number (EISSN)

  • 1614-5054

abstract

  • This article details advances in a lightweight technology we have evolved to handle post hoc verification in the very large, uncontrolled and rapidly evolving code-bases exemplified by C language open source projects such as the Linux kernel. Successful operation in this context means timeliness, and we are currently treating millions of lines of unrestricted mixed C and assembler source code in a few hours on very modest platforms. The technology is soundly based, in that it delivers false alarms (in a ratio of about 8 to 1 in practice), rather than misses true alarms. Speed of operation is traded off against accuracy via configuration of a program logic tailored to each analysis. The program logic specification language and the theory behind it will be described here.