Compares our linear programming technology for software verification (LPV) with other verification systems: explicit exploration using partial order reduction (Spin) and implicit exploration using BDDs (Xeve/Esterel). The case study is a safety property of an easily-scalable problem (a bus arbiter). The results show that exploration-based methods (Spin and Xeve/Esterel) have an overall exponential complexity, restricting their use on small instances. The LPV technique, which does not rely on exploration, is the only one fast enough (quadratic complexity) to handle systems that are 50 times larger than the other techniques presented in this paper can do. Moreover, in opposition to exploration-based methods, LPV produces real proven facts that mean this technique shares some common points with theorem proving. We believe that the scale-change robustness of LPV shows that linear programming can be applied successfully to the verification of industrial systems.
展开▼
