Computer-Assisted Assume/Guarantee Reasoning with VeriSoft

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.

• Type: Conference
• Year: 2003
• Where: ICSE
• Authors: Jürgen Dingel
• Keywords: ICSE 2003, Software Engineering