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.
展开▼
机译：我们展示了如何使用状态空间探索工具Verisoft如何合成分析并行C / C ++程序。 Verisoft用于自动检查采用/保证并行过程的规格。分析意味着补充标准假设/保证推理，这通常仅与“铅笔和纸张”进行。虽然成功分析并不总是暗示规范的一般正确性，但它会增加对验证工作的信心。不成功的分析始终产生一个反例，可用于校正规范或程序。 Verisoft的优化和可视化技术使分析相对效率和有效。
展开▼
