The Importance of Non-theorems and Counterexamples in Program Verification (bibtex)
by Graham Steel
Abstract:
We argue that the detection and refutation of non-theorems, and the discovery of appropriate counterexamples, is of vital importance to the Grand Challenge of a Program Verifier.
Reference:
The Importance of Non-theorems and Counterexamples in Program Verification (Graham Steel), In Revised Selected Papers and Discussions of the 1st IFIP TC2\slashWG2.3 Conference Verified Software---Theories, Tools, and Experiments (VSTTE'05) (Bertrand Meyer, Jim Woodcock, eds.), Springer, volume 4171, 2008.
Bibtex Entry:
@inproceedings{steel05-vstte,
  abstract =      {We argue that the detection and refutation of
                   non-theorems, and the discovery of appropriate
                   counterexamples, is of vital importance to the Grand
                   Challenge of a Program Verifier.},
  address =       {Zurich, Switzerland},
  author =        {Steel, Graham},
  booktitle =     {{R}evised {S}elected {P}apers and {D}iscussions of
                   the 1st {IFIP} {TC2}\slash{WG2.3} {C}onference
                   {V}erified {S}oftware---{T}heories, {T}ools, and
                   {E}xperiments ({VSTTE}'05)},
  DOI =           {10.1007/978-3-540-69149-5_53},
  editor =        {Meyer, Bertrand and Woodcock, Jim},
  pages =         {491-495},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {The Importance of Non-theorems and Counterexamples in
                   Program Verification},
  volume =        {4171},
  year =          {2008},
  acronym =       {{VSTTE}'05},
  conf-year =     {2005},
  conf-month =    oct,
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/steel-vstte05.pdf},
  PDF =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/steel-vstte05.pdf},
  lsv-category =  {intc},
  lsv-time =      {ant},
  wwwpublic =     {perso},
}
Powered by bibtexbrowser