作者:
J Dingel
关键词:
formal specification ； parallel programming ； program verification ； program visualisation ； VeriSoft ； formal specification ； formal verification ； optimization ； parallel processes ； state space exploration tool
摘要:
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.
在线下载