Specifying and verifying software

Abstract

Software verification presents many challenges. One of these isproviding programmers with automated tool support for verification, another is providing specification support that captures common programming idioms. In this talk, I will discuss these two challenges, drawing from experience with building program verifiersfor Spec# and C. I will also give a demo of the Spec# programming system, which includes the automatic static program verifier Boogie.

BibTeX

@inproceedings{Leino:ASE07,
  author    = {K. Rustan M. Leino},
  title     = {Specifying and verifying software},
  booktitle = {ASE},
  pages     = {2},
  publisher = {{ACM}},
  year      = {2007},
}

Specifying and verifying software

Abstract

Related papers