Abstract interpretation of reactive systems

ACM Transactions on Programming Languages and Systems - Tập 19 Số 2 - Trang 253-291 - 1997
Dennis Dams1, Rob Gerth1, Orna Grumberg2
1Eindhoven Univ. of Technology, Eindhoven, The Netherlands
2Technion–Israel Institute of Technology, Haifa, Israel

Tóm tắt

Từ khóa


Tài liệu tham khảo

BACK R. J., 1983, the 2nd A CM SIGA CT-SIGOPS Symposium on Principles of Distributed Computing. ACM, 131

BENSALEM S., 1992, Eds. Lecture Notes in Computer Science, 663, 251

10.1016/0167-6423(92)90018-7

10.1145/5397.5399

CLARKE E., 1992, the 19th Annual A CM SIGPLAN-SIGA CT Symposium on Principles of Programming Languages. ACM SIGACT/SIGPLAN

10.1145/186025.186051

CLEAVELAND R., 1994, Eds. Lecture Notes in Computer Science, 836, 417

CLEAVELAND R., 1995, Ed. Lecture Notes in Computer Science, 983, 51

10.1145/177492.177656

COUSOT P., 1977, Proceedings of the Jth ACM Symposium on Principles of Programming Languages. ACM, 238

COUSOT P., 1979, Proceedings of the 6th A CM Symposium on Principles of Programming Languages. ACM, 269

10.1016/0743-1066(92)90030-7

COUSOT P., 1992, Abstract interpretation frameworks, J. Logic Comput., 2, 511, 10.1093/logcom/2.4.511

10.1016/0304-3975(94)90269-0

DAMM W., 1995, Statecharts: Using graphical specification languages and symbolic model checking in the verification of a production cell. In Formal Development of Reactive Systems: Case Study Production Cell

DAMS D., Computer Aided Verification

DAMS D., Computer Aided Verification

DAMS D. GRUMBERG O. AND GERTH R. 1993b. Abstract interpretation of reactive systems: Abstractions preserving ACTL* ECTL* and CTL*. Dept. of Mathematics and Computing Science Eindhoven Univ. of Technology Eindhoven The Netherlands. DAMS D. GRUMBERG O. AND GERTH R. 1993b. Abstract interpretation of reactive systems: Abstractions preserving ACTL* ECTL* and CTL*. Dept. of Mathematics and Computing Science Eindhoven Univ. of Technology Eindhoven The Netherlands.

DAMS D. GRUMBERG O. AND GERTH R. 1995. Abstract interpretation of reactive systems: Preservation of CTL* Logic Group Preprint Series 132 Dept. of Philosophy Utrecht Univ. Utrecht The Netherlands. May. Also appeared as Computing Science Note 95/16 Dept. of Mathematics and Computing Science Eindhoven Univ. of Technology. DAMS D. GRUMBERG O. AND GERTH R. 1995. Abstract interpretation of reactive systems: Preservation of CTL* Logic Group Preprint Series 132 Dept. of Philosophy Utrecht Univ. Utrecht The Netherlands. May. Also appeared as Computing Science Note 95/16 Dept. of Mathematics and Computing Science Eindhoven Univ. of Technology.

DAMS D. R. 1996. Abstract interpretation and partition refinement for model checking. Ph.D. thesis Eindhoven Univ. of Technology Eindhoven The Netherlands. DAMS D. R. 1996. Abstract interpretation and partition refinement for model checking. Ph.D. thesis Eindhoven Univ. of Technology Eindhoven The Netherlands.

DE FRANCESCO N., Tools and Algorithms for the Construction and Analysis of Systems

DILL D. 1989. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. The MIT Press London. DILL D. 1989. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. The MIT Press London.

10.1145/4904.4999

GINZBURG A. 1968. Algebraic Theory of Automata. ACM Monograph Series. Academic Press New York/London. GINZBURG A. 1968. Algebraic Theory of Automata. ACM Monograph Series. Academic Press New York/London.

GRAF S., Computer Aided Verification

GRAF S., Computer Aided Verification

10.1016/0167-6423(87)90035-9

HENNESSY M., 1980, Proceedings of the 7th International Colloquium on Automata Languages and Programming (ICALP), J. de Bakker and J. van Leeuwen, Eds. Lecture Notes in Computer Science, 85, 299

KELB P. 1994. Model checking and abstraction: A framework preserving both truth and failure information. Carl yon Ossietzky Univ. of Oldenburg Oldenburg Germany. Unpublished note. KELB P. 1994. Model checking and abstraction: A framework preserving both truth and failure information. Carl yon Ossietzky Univ. of Oldenburg Oldenburg Germany. Unpublished note.

KELB P. 1995. Abstraktionstechniken fiir automatische verifikationsmethoden. Ph.D. thesis Carl yon Ossietzky Univ. of Oldenburg Oldenburg Germany. KELB P. 1995. Abstraktionstechniken fiir automatische verifikationsmethoden. Ph.D. thesis Carl yon Ossietzky Univ. of Oldenburg Oldenburg Germany.

KELB P. DAMS D. AND GERTH R. 1995. Efficient symbolic model checking of the full >- calculus using compositional abstractions. Computing Science Rep. 95/31 Eindhoven Univ. of Technology Eindhoven The Netherlands. Oct. KELB P. DAMS D. AND GERTH R. 1995. Efficient symbolic model checking of the full >- calculus using compositional abstractions. Computing Science Rep. 95/31 Eindhoven Univ. of Technology Eindhoven The Netherlands. Oct.

KOZEN D., 1983, Results on the propositional #-calculus, Theor. Comput. Sci., 27, 333, 10.1016/0304-3975(82)90125-6

KRIPKE S., 1963, A semantical analysis of modal logic I: Normal modal propositional calculi, Zeitschrift fiir Mathematische Logik und Grundlagen der Mathematik, 9, 67, 10.1002/malq.19630090502

KURSHAN R. P., Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, J. W. de Bakker, W.-P

KURSHAN R. P. 1994. Computer-Aided Verification of Coordinating Processes: The Automata- Theoretic Approach . Princeton Series in Computer Science . Princeton University Press Princeton N.J. KURSHAN R. P. 1994. Computer-Aided Verification of Coordinating Processes: The Automata- Theoretic Approach. Princeton Series in Computer Science. Princeton University Press Princeton N.J.

LARSEN K. G., 1989, Ed. Lecture Notes in Computer Science, 407, 232

LARSEN K. G., 1988, the 1988 IEEE Symposium on Logic in Computer Science. IEEE Computer Society, Washington, D.C., 203-210

LICHTENSTEIN O., 1985, the 12th Annual ACM Symposium on Principles of Programming Languages. ACM SIGACT/SIGPLAN, 97

LOISEAUX C. 1994. V6rification symbolique de syst~mes r6actifs g l'aide d'abstractions. Ph.D. thesis Universit6 Joseph Fourier- Grenoble I Grenoble France. LOISEAUX C. 1994. V6rification symbolique de syst~mes r6actifs g l'aide d'abstractions. Ph.D. thesis Universit6 Joseph Fourier- Grenoble I Grenoble France.

10.1007/BF01384313

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.

10.1007/BF01178576

MILNER R., 1971, the 2nd International Joint Conference on Artificial Intelligence. British Computer Society, 481

PARK D., 1981, Ed. Lecture Notes in Computer Science, 104, 167

QUEILLE J. P., 1982, International Symposium on Programming, M. Dezani-Ciancaglini and U. Montanari, Eds. Lecture Notes in Computer Science, 137, 337

SIFAKIS J. 1982. Property preserving homomorphisms and a notion of simulation for transition systems. Rapport de Recherche 332 IMAG Grenoble France. Nov. SIFAKIS J. 1982. Property preserving homomorphisms and a notion of simulation for transition systems. Rapport de Recherche 332 IMAG Grenoble France. Nov.

SIFAKIS J., 1983, Eds. Lecture Notes in Computer Science, 164, 458

VAN BENTHEM J., 1994, Modal logic, transition systems and processes, J. Logic Comput., 4, 811, 10.1093/logcom/4.5.811

VARDI M. Y., Logic in Computer Science