Model checking and abstraction
Tóm tắt
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 10 1300 states.
Từ khóa
Tài liệu tham khảo
BEATTY D. L., 1991, Proceedings of the 28th Design Automation Conference. IEEE Computer Society Press, Los Alamitos, Calif., 397-402
BENSALEM S., 1992, Proceedings of the 4th Workshop on Computer-Aided Verification, G. V. Bochmann and D. K. Probst, Eds. Lecture Notes in Computer Science, 663, 260
BURCH J. R., 1991, Proceedings of the 28th Design Automation Conference. IEEE Computer Society Press, Los Alamitos, Calif., 403-407
BURCH J. R., 1990, Proceedings of the 27th Design Automation Conference. IEEE Computer Society Press, Los Alamitos, Calif., 46-51
CLARKE E. M., 1981, Logic of Programs: Workshop, 131
CLARKE E. M., 1990, Proceedings of the 1990 IEEE International Conference on Computer Design. IEEE Computer Society Press, Los Alamitos, Calif., 220-223
CLARKE, 1983, Proceedings of the lOth Annual ACM Symposium on Principles of Programming Languages, 117
CLARKE E. M., 1989, Compositional model checking. }in Proceedings of the 4th Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 46
CLEAVELAND R., 1990, Tableau-based model checking in the propositional mucalculus, Acta Inf., 27, 8, 10.1007/BF00264284
COUDER O., 1990, Proceedings of the 1990 International Conference on Computer-Aided Design. IEEE Computer Society Press, Los Alamitos, Calif., 126-129
COUSOT P., 1979, Proceedings of the 6th Annual ACM Symposium on Principles of Programming Languages (San Antonio, Tx. Jan.). ACM, 269
COUSOT, 1977, Proceedings of the 4~h Annual ACM Symposium on Principles of Programming Languages, 238
DILL D. L. 1989. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations MIT Press Cambridge Mass. DILL D. L. 1989. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations MIT Press Cambridge Mass.
FLOYD R. W., 1967, Proceedings of the Symposium on Applied Mathematics 19 (Mathematical Aspects of Computer Science), J. T. Schwartz, Ed. American Mathematical Society, Providence, R.I.
FUJITA M., 1988, Proceedings of the 1988 Internationail Conference on Computer-Aided Design (Santa Clara, Calif. Nov.). IEEE Computer Society Press, Los Alamitos, Calif., 2-5.
GRAF S., 1990, Proceedings of the 1990 Workshop on Computer-Aided Verification, 186
GRUMBERG O., 1991, Proceedings of CONCUR 91: 2nd International Conference on Concurrency Theory, J. C. M. Baeten and J. F. Groote, Eds. Lecture Notes in Computer Science, 527, 250, 10.1007/3-540-54430-5_93
GUNTER C. A., Handbook of Theoretical Computer Science
HAR'EL Z., 1987, The COSPAN user's guide, Tech. Rep. 11211-871009-21TM, AT&T Bell Laboratories, Murray Hill, N.J.
JOSKO B., Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, J. W. de Bakker, W.-P
KURSHAN R. P., Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, J. W. de Bakker, W.-P
LICHTENSTEIN O., 1985, Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages, 97
LONG D. E. 1993. Model checking abstraction and compositional verification. Ph.D. thesis School of Computer Science Carnegie Mellon Univ. Pittsburgh Pa. LONG D. E. 1993. Model checking abstraction and compositional verification. Ph.D. thesis School of Computer Science Carnegie Mellon Univ. Pittsburgh Pa.
MYCROFT A. 1981. Abstract interpretation and optimizing transformations for applicative programs. Ph.D. thesis Dept. of Computer Science Univ. of Edinburgh Scotland. MYCROFT A. 1981. Abstract interpretation and optimizing transformations for applicative programs. Ph.D. thesis Dept. of Computer Science Univ. of Edinburgh Scotland.
NIELSON F., 1982, A denotationat framework for data flow analysis, Acta Inf., 18, 3, 10.1007/BF00263194
QUIELLE J., 1981, Proceedings of the 5th International Symposium in Programming.
SHUREK G., 1990, Proceedings of the 1990 Workshop on Computer-Aided Verification, 214
TOUAT, 1990, Proceedings of the 1990 International Conference on Computer-Aided Design. IEEE Computer Society Press, Los Alamitos, Calif., 130-133
WOLPER P., 1986, Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages (St