Automatic reduction in CTL compositional model checking

1. R. E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Trans. on Computers, C-35(8), pp. 677–691, Aug. 1986.

   Google Scholar 

2. J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, “Sequential Circuit Verification Using Symbolic Model Checking,” in Proc. of 27th Design Automation Conference, pp. 46–51, June 1990.

   Google Scholar 

3. J. R. Burch, E. M. Clarke, and D. E. Long, “Representing Circuits More Efficiently in Symbolic Model Checking,” in Proc. of 28th Design Automation Conference, pp. 403–407, June 1991.

   Google Scholar 

4. M. Chiodo, T. R. Shiple, A. Sangiovanni-Vincentelli, and R. K. Brayton, “Automatic Reduction in CTL Compositional Model Checking,” Memorandum No. UCB/ERL M92/55, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, Jan. 1992.

   Google Scholar 

5. E. M. Clarke, E. A. Emerson, and P. Sistla, “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,” ACM Trans. Prog. Lang. Syst., 8(2), pp. 244–263, 1986.

   Google Scholar 

6. E. M. Clarke, D. E. Long, and K. L. McMillan, ‘Compositional Model Checking,’ in Proc. of the 4th Annual Symposium on Logic in Computer Science, Asilomar, CA, June 1989.

   Google Scholar 

7. E. M. Clarke, O. Grumberg and D. E. Long, “Model Checking and Abstraction,” in Proc. of Principles of Programming Languages, Jan. 1992.

   Google Scholar 

8. O. Coudert, C. Berthel, and J. C. Madre, “Verification of Synchronous Sequential Machines Based on Symbolic Execution,” in Lecture Notes in Computer Science: Automatic Verification Methods for Finite State Systems, vol. 407, editor J. Sifakis, Springer-Verlag, pp. 365–373, June 1989.

   Google Scholar 

9. S. Graf and B. Steffen, “Compositional Minimization of Finite State Systems,” in Lecture Notes in Computer Science: Proc. of the 1990 Workshop on Computer-Aided Verification, vol. 531, editors R. P. Kurshan and E. M. Clarke, Springer-Verlag, pp. 186–196, June 1990.

   Google Scholar 

10. O. Grumberg and D. E. Long, “Model Checking and Modular Verification,” in Lecture Notes in Computer Science: Proc. CONCUR '91: 2nd Inter. Conf. on Concurrency Theory, vol. 527, editors J. C. M. Baeten and J. F. Groote, Springer-Verlag, Aug. 1991.

    Google Scholar 

11. J. E. Hopcroft, “An n log n Algorithm for Minimizing the States in a Finite Automaton,” in The Theory of Machines and Computation, New York: Academic Press, pp. 189–196, 1971.

    Google Scholar 

12. R. P. Kurshan and K. L. McMillan, “A Structural Induction Theorem for Processes,” in Proc. of 8th ACM Symp. on Principles of Distributed Computing, Aug. 1989.

    Google Scholar 

13. R. P. Kurshan, “Analysis of Discrete Event Coordination,” in Lecture Notes in Computer Science: Proc. REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, vol. 430, editors J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, Springer-Verlag, May 1989.

    Google Scholar 

14. E. M. Sentovich, K. J. Singh, C. Moon, H. Savoj, R. K. Brayton, and A. Sangiovanni-Vincentelli, “Sequential Circuit Design Using Synthesis and Optimization,” in Proc. of International Conference on Computer Design, Oct. 1992.

    Google Scholar 

15. H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli, “Implicit State Enumeration of Finite State Machines using BDDs,” in Proc. of IEEE International Conference on Computer-Aided Design, pp. 130–133, Nov. 1990.

    Google Scholar 

16. P. Wolper and V. Lovinfosse, “Verifying Properties of Large Sets of Processes with Network Invariants,” in Lecture Notes in Computer Science: Automatic Verification Methods for Finite State Systems, vol. 407, editor J. Sifakis, Springer-Verlag, pp. 68–80, June 1989.

    Google Scholar 

Download references