Proof-guided underapproximation-widening for multi-process systems

ABSTRACT

This paper presents a procedure for the verification of multi-process systems based on considering a series of underapproximated models. The procedure checks models with an increasing set of allowed interleavings of the given set of processes, starting from a single interleaving. The procedure relies on SAT solvers' ability to produce proofs of unsatisfiability: from these proofs it derives information that guides the process of adding interleavings on the one hand, and determines termination on the other. The presented approach is integrated in a SAT-based Bounded Model Checking (BMC) framework. Thus, a BMC formulation of a multi-process system is introduced, which allows controlling which interleavings are considered. Preliminary experimental results demonstrate the practical impact of the presented method.

REFERENCES

• 1: Rajeev Alur , Robert K. Brayton , Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani, Partial-Order Reduction in Symbolic State Space Exploration, Proceedings of the 9th International Conference on Computer Aided Verification, p.340-351, June 22-25, 1997
• 2: N. Amla and K. McMillan. Automatic abstraction without counterexamples. In H. Garavel and J. Hatcliff, editors, 9th Intl. Conf. on Tools And Algorithms For The Construction And Analysis Of Systems (TACAS'03), volume 2619 of Lect. Notes in Comp. Sci., 2003.
• 3: Felice Balarin , Alberto L. Sangiovanni-Vincentelli, An Iterative Approach to Language Containment, Proceedings of the 5th International Conference on Computer Aided Verification, p.29-40, June 28-July 01, 1993
• 4: Sharon Barner , Daniel Geist , Anna Gringauze, Symbolic Localization Reduction with Reconstruction Layering and Backtracking, Proceedings of the 14th International Conference on Computer Aided Verification, p.65-77, July 27-31, 2002
• 5: Sharon Barner , Orna Grumberg, Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.93-106, July 27-31, 2002
• 6: A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zue. Bounded Model Checking, volume~58 of Advances in computers. Academic Press, 2003.
• 7: A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States [doi>10.1145/309847.309942]
• 8: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 9: Pankaj Chauhan , Edmund M. Clarke , James H. Kukula , Samir Sapra , Helmut Veith , Dong Wang, Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.33-51, November 06-08, 2002
• 10: Edmund Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM (JACM), v.50 n.5, p.752-794, September 2003 [doi>10.1145/876638.876643]
• 11: Edmund M. Clarke , Anubhav Gupta , James H. Kukula , Ofer Shrichman, SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques, Proceedings of the 14th International Conference on Computer Aided Verification, p.265-279, July 27-31, 2002
• 12: E. Clarke, D. Kroening, J. Ouaknine, and O. Strichman. Completeness and complexity of bounded model checking. In Proc. 5th Intl. Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), volume 2937 of Lect. Notes in Comp. Sci., pages 85--96, Venice, Italy, Jan 2004.
• 13: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 14: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 15: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 16: Marcelo Glusman , Shmuel Katz, A Mechanized Proof Environment for the Convenient Computations Proof Method, Formal Methods in System Design, v.23 n.2, p.115-142, September 2003 [doi>10.1023/A:1024746015231]
• 17: Patrice Godefroid , Pierre Wolper, Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.332-342, July 01-04, 1991
• 18: Shmuel Katz , Doron Peled, Verification of distributed programs using representative interleaving sequences, Distributed Computing, v.6 n.2, p.107-120, September 1992 [doi>10.1007/BF02252682]
• 19: Daniel Kroening , Ofer Strichman, Efficient Computation of Recurrence Diameters, Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, p.298-309, January 09-11, 2002
• 20: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 21: Robert P. Kurshan , Vladimir Levin , Marius Minea , Doron Peled , Hüsnü Yenigün, Combining Software and Hardware Verification Techniques, Formal Methods in System Design, v.21 n.3, p.251-280, November 2002 [doi>10.1023/A:1020383505582]
• 22: Jørn Lind-Nielsen , Henrik Reif Andersen, Stepwise CTL Model Checking of State/Event Systems, Proceedings of the 11th International Conference on Computer Aided Verification, p.316-327, July 06-10, 1999
• 23: K. L. McMillan. Interpolation and sat-based model checking. In J. Warren A. Hunt and F. Somenzi, editors, cav03, Lect. Notes in Comp. Sci., Jul 2003.
• 24: Doron Peled, Combining Partial Order Reductions with On-the-fly Model-Checking, Proceedings of the 6th International Conference on Computer Aided Verification, p.377-390, June 21-23, 1994
• 25: Kavita Ravi , Fabio Somenzi, High-density reachability analysis, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.154-158, November 05-09, 1995, San Jose, California, United States
• 26: Kavita Ravi , Fabio Somenzi, Hints to accelerate Symbolic Traversal, Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.250-264, September 27-29, 1999
• 27: Mary Sheeran , Satnam Singh , Gunnar Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.108-125, November 01-03, 2000
• 28: Antti Valmari, A Stubborn Attack On State Explosion, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.156-165, June 18-21, 1990

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

General Terms:
Algorithms, Reliability, Verification

Keywords:
SAT proofs, abstraction, bounded model checking, software verification, underapproximation-widening