Combining Software and Hardware Verification Techniques

1. R. Alur, R.K. Brayton, T.A. Henzinger, S. Qadeer, and S.K. Rajamani, “Partial-order reduction in symbolic state space exploration,” in O. Grumberg (ed.), Computer Aided Verification, 9th International Conference, (CAV '97) Proceedings, Vol. 1254 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1997, pp. 340-351.

   Google Scholar 

2. B. Berger and P.W. Shor, “Approximation algorithms for the maximum acyclic subgraph problem,” in First ACM-SIAM Symp. on Discrete Algorithms. Proceedings, 1990, pp. 236-243.

3. C.-T. Chou and D. Peled, “Formal verification of a partial-order reduction technique for model checking,” in T. Margaria and B. Steffen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Second InternationalWorkshop (TACAS '96) Proceedings, Vol. 1055 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1996, pp. 241-257.

   Google Scholar 

4. D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, Cambridge, MA, 1989.

   Google Scholar 

5. D. Dolev, M. Klawe, and M. Rodeh, “An O(n log n) unidirectional distributed algorithm for extrema finding in a circle,” Journal of Algorithms, Vol. 3, No. 3, pp. 245-260, 1982.

   Google Scholar 

6. P. Eades, X. Lin, and W.M. Smyth, “Afast and effective heuristic for the feedback arc set problem,” Information Processing Letters, Vol. 47, No. 6, pp. 319-323, 1993.

   Google Scholar 

7. D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, “On the temporal analysis of fairness,” in Conference Record of the Seventh ACM Symposium on Principles of Programming Languages, 1980, pp. 163-173.

8. P. Godefroid and D. Pirottin, “Refining dependencies improves partial-order verification methods,” in C. Courcoubetis (Ed.), Computer Aided Verification, 5th International Conference (CAV '93) Proceedings, Vol. 697 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1993, pp. 438-449.

   Google Scholar 

9. R.H. Hardin, Z. Har'El, and R.P. Kurshan, “COSPAN,” in R. Alur and T.A. Henzinger (Eds.), Computer Aided Verification, 8th International Conference (CAV '96) Proceedings, Vol. 1102 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1996, pp. 423-427.

   Google Scholar 

10. Z. Har'El and R.P. Kurshan, “Software for analytical development of communication protocols,” AT&T Technical Journal, Vol. 69, No. 1, pp. 45-59, 1990.

    Google Scholar 

11. G.J. Holzmann, “The model checker Spin,” IEEE Trans. on Software Engineering,Vol. 23, No. 5, pp. 279-295, 1997.

    Google Scholar 

12. G.J. Holzmann and D. Peled, “An improvement in formal verification,” in D. Hogrefe and S. Leue (Eds.), Formal Description Techniques VII, Proceedings of the 7th IFIP WG 6.1 International Conference Bern, Switzerland, 1994, pp. 197-211.

13. R.M. Karp, “Reducibility among combinatorial problems,” in Complexity of Computer Computations, Plenum Press, New York, 1972, pp. 85-103.

    Google Scholar 

14. R.P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press, Princeton, NJ, 1994.

    Google Scholar 

15. R. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün, “Static partial order reduction,” in B. Steffen (Ed.), Tools and Algorithms for the Construction and Analysis of Systems, 4th International Conference (TACAS'98) Proceedings, Vol. 1384 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1998, pp. 345-357.

    Google Scholar 

16. R.P. Kurshan, M. Merritt, A. Orda, and S. Sachs, “Modeling asynchrony with a synchronous model,” in P. Wolper (Ed.), Computer Aided Verification, 7th International Conference (CAV'95) Proceedings, Vol. 939 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995, pp. 339-352.

    Google Scholar 

17. L. Lamport, “What good is temporal logic,” in R.E.A. Mason (Ed.), Proceedings of IFIP Congress, North Holland, 1983, pp. 657-668.

18. V. Levin, E. Bounimova, O. Başbuğoğlu, and K. İnan, “A verifiable software/hardware co-design using SDL and COSPAN,” in Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, Maribor, Slovenia, 1996, pp. 6-16.

19. V. Levin and H. Yenigün, “SDLCheck: A model checking tool,” in G. Berry, H. Comon, and A. Finkel (Eds.), Computer Aided Verification, 13th International Conference (CAV 2001) Proceedings, Vol. 2102 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 2001, pp. 378-381.

    Google Scholar 

20. K.L. McMillan, Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1993.

    Google Scholar 

21. D. Peled, “Combining partial order reductions with on-the-fly model-checking,” Formal Methods in System Design, Vol. 8, pp. 39-64, 1996.

    Google Scholar 

22. D. Peled and T. Wilke, “Stutter-invariant temporal properties are expressible without the next-time operator,” Information Processing Letters, Vol. 63, No. 5, pp. 243-246, 1997.

    Google Scholar 

23. SDL92, “Functional specification and description language (SDL), ITU-T Recommendation Z.100,” 1993, Geneva.

24. N. Sharygina, R.P. Kurshan, and J.C. Browne, “A formal object-oriented analysis for software reliability: Design for verification,” in Heinrich Husmann (Ed.), Fundamental Approaches to Software Engineering, 4th International Conference (FASE 2001) Proceedings, Vol. 2029 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 2001, pp. 318-332.

    Google Scholar 

25. S. Shlaer and S.J. Mellor, Object Lifecycles Modeling the World in States, Prentice-Hall, Englewood Cliffs, NJ, 1992.

    Google Scholar 

26. A. Valmari, “A stubborn attack on state explosion,” in E.M. Clarke and R.P. Kurshan (Eds.), Computer-Aided Verification, 2nd International Conference (CAV '90) Proceedings, Vol. 531 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1990, pp. 156-165.

    Google Scholar 

27. Verilog95, “IEEE standard hardware description language based on the Verilog^TM hardware description language, “IEEE Std 1364-1995,” 1996, New York.

28. VHDL93, “IEEE Standard VHDL Language Reference Manual, IEEE Std 1076-1993,” 1994, New York.

Download references