kirancodes.me
To Proof Maintenance & Beyond!
ASE 2008

PtYasm: Software Model Checking with Proof Templates

Thomas E. Hart, Kelvin Ku, Arie Gurfinkel, Marsha Chechik, David Lie

DOI 10.1109/ase.2008.80dblp

Abstract

We describe PTYASM, an enhanced version of the YASM software model checker which uses proof templates. These templates associate correctness arguments with common programming idioms, thus enabling efficient verification. We have used PTYASM to verify the safety of array accesses in programs derived from the Verisec suite. PTYASM is able to verify this property in the majority of testcases, while existing software model checkers fail to do so due to loop unrolling.

BibTeX
@inproceedings{Hart-al:ASE08,
  author    = {Thomas E. Hart and
               Kelvin Ku and
               Arie Gurfinkel and
               Marsha Chechik and
               David Lie},
  title     = {{PtYasm:} Software Model Checking with Proof Templates},
  booktitle = {ASE},
  pages     = {479--480},
  publisher = {{IEEE} Computer Society},
  year      = {2008},
}

Related papers