Computer-Assisted Assume/Guarantee Reasoning with VeriSoft

DOI 10.1109/icse.2003.1201195 dblp

Abstract

We show how the state space exploration tool VeriSoft can be used to analyze parallel C/C++ programs compositionally. VeriSoft is used to check assume/guarantee specifications of parallel processes automatically. The analysis is meant to complement standard assume/guarantee reasoning which is usually carried out solely with "pencil and paper". While a successful analysis does not always imply the general correctness of the specification, it increases the confidence in the verification effort. An unsuccessful analysis always produces a counterexample which can be used to correct the specification or the program. VeriSoft's optimization and visualization techniques make the analysis relatively efficient and effective.

BibTeX

@inproceedings{Dingel:ICSE03,
  author    = {J{\"{u}}rgen Dingel},
  title     = {{Computer-Assisted} {Assume/Guarantee} Reasoning with {VeriSoft}},
  booktitle = {ICSE},
  pages     = {138--148},
  publisher = {{IEEE} Computer Society},
  year      = {2003},
}

Computer-Assisted Assume/Guarantee Reasoning with VeriSoft

Abstract

Related papers