Model checking and abstraction

ABSTRACT

We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a program representing a pipelined ALU circuit with over 101300 states.

REFERENCES

• 1: Randal E. Bryant , Derek L. Beatty , Carl-Johan H. Seger, Formal hardware verification by symbolic ternary trajectory evaluation, Proceedings of the 28th conference on ACM/IEEE design automation, p.397-402, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127701]
• 2: Saddek Bensalem , Ahmed Bouajjani , Claire Loiseaux , Joseph Sifakis, Property Preserving Simulations, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.260-273, June 29-July 01, 1992
• 3: M C Browne , E M Clarke , D L Dill , B Mishra, Automatic verification of sequential circuits using temporal logic, IEEE Transactions on Computers, v.35 n.12, p.1035-1044, Dec. 1986 [doi>10.1109/TC.1986.1676711]
• 4: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 5: J. R. Burch , E. M. Clarke , D. E. Long, Representing circuits more efficiently in symbolic model checking, Proceedings of the 28th conference on ACM/IEEE design automation, p.403-407, June 17-22, 1991, San Francisco, California, United States [doi>10.1145/127601.127702]
• 6: J. R. Burch , E. M. Clarke , K. L. McMillan , David L. Dill, Sequential circuit verification using symbolic model checking, Proceedings of the 27th ACM/IEEE conference on Design automation, p.46-51, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123223]
• 7: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 8: CLARKE.. E. M., AND I~MURA, S. 1990. A parallel algorithm for constructing binary decision diagrams. In Proceedings of the 1990 IEEE International Conference on Computer Design. IEEE Computer Society Press, Los Alamitos, Calif., 220-223.
• 9: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 10: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.117-126, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567080]
• 11: E. Clarke , D. Long , K. McMillan, Compositional model checking, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.353-362, June 1989, Pacific Grove, California, United States
• 12: R. Cleaveland, Tableau-based model checking in the propositional mu-calculus, Acta Informatica, v.27 n.9, p.725-747, Sep. 1990
• 13: COUDER% O., AND MADRE, J. C. 1990. A unified framework for the formal verification of sequential circuits. In Proceedings of the 1990 International Conference on Computer-Aided Design. IEEE Computer Society Press, Los Alamitos, Calif., 126-129.
• 14: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 15: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 16: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, MIT Press, Cambridge, MA, 1989
• 17: FLOYD, R. W. 1967. Assigning meanings to programs. In Proceedings of the Symposium on Applied Mathematics 19 (Mathematical Aspects of Computer Science), J. T. Schwartz, Ed. American Mathematical Society, Providence, R.I.
• 18: FUJITA, M., FUJISAWA, H., AND KAWATO, N. 1988. Evaluation and improvements of Boolean comparison method based on binary decision diagrams. In Proceedings of the 1988 Internationail Conference on Computer-Aided Design (Santa Clara, Calif. Nov.). IEEE Computer Society Press, Los Alamitos, Calif., 2-5.
• 19: Susanne Graf , Bernhard Steffen, Compositional Minimization of Finite State Systems, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.186-196, June 18-21, 1990
• 20: Orna Grumberg , David E. Long, Model Checking and Modular Verification, Proceedings of the 2nd International Conference on Concurrency Theory, p.250-265, August 26-29, 1991
• 21: C. A. Gunter , D. S. Scott, Semantic domains, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 22: HAR'EL, Z.,ANDKURSHAN, R.P. 1987. The COSPAN user's guide. Tech. Rep. 11211-871009-21TM, AT&T Bell Laboratories, Murray Hill, N.J.
• 23: B. Josko, Verifying the correctness of AADL modules using model checking, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.386-400, May 1990, Mook, The Netherlands
• 24: R. P. Kurshan, Analysis of discrete event coordination, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.414-453, May 1990, Mook, The Netherlands
• 25: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 26: David Esley Long, Model checking, abstraction, and compositional verification, Carnegie Mellon University, Pittsburgh, PA, 1993
• 27: MYCROFT, A. 1981. Abstract interpretation and optimizing transformations for applicative programs. Ph.D. thesis, Dept. of Computer Science, Univ. of Edinburgh, Scotland.
• 28: NIELSON, F. 1982. A denotationat framework for data flow analysis. Acta Inf. 18, 3 (Dec.), 265-287.
• 29: QUIELLE, J., AND SIFAKI{S, J. 1981. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th International Symposium in Programming.
• 30: Gil Shurek , Orna Grumberg, The Modular Framework of Computer-Aided Verification, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.214-223, June 18-21, 1990
• 31: A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985 [doi>10.1145/3828.3837]
• 32: TOUATt, H., SAVOJ, H., LIN, B., BRAYTON, R. K., AND SANGIOVANNI-VINCENTELLI, A. 1990. Implicit state enumeration of finite state machines using BDD's. In Proceedings of the 1990 International Conference on Computer-Aided Design. IEEE Computer Society Press, Los Alamitos, Calif., 130-133.
• 33: Pierre Wolper, Expressing interesting properties of programs in propositional temporal logic, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.184-193, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512661]

INDEX TERMS

Primary 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

Additional Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids
          Subjects: Verification

  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Verification

Keywords:
abstract interpretation, binary decision diagrams (BDDs), model checking, temporal logic