Abstract and Model Check While You Prove

作者: Hassen Saïdi , Natarajan Shankar

DOI: 10.1007/3-540-48683-6_38

关键词:

摘要: The construction of abstractions is essential for reducing large or infinite state systems to small or finite state systems. Boolean abstractions, where boolean variables replace concrete …

参考文章(11)
Susanne Graf, Hassen Saidi, Construction of Abstract State Graphs with PVS computer aided verification. pp. 72- 83 ,(1997) , 10.1007/3-540-63166-6_10
S. Rajan, N. Shankar, M. K. Srivas, An Integration of Model Checking with Automated Proof Checking computer aided verification. pp. 84- 97 ,(1995) , 10.1007/3-540-60045-0_42
Klaus Havelund, Natarajan Shankar, Experiments in Theorem Proving and Model Checking for Protocol Verification formal methods. pp. 662- 681 ,(1996) , 10.1007/3-540-60973-3_113
Friedrich W. von Henke, Stephan Pfab, Holger Pfeifer, Harald Rue\, Case Studies in Meta-Level Theorem Proving theorem proving in higher order logics. pp. 461- 478 ,(1998) , 10.1007/BFB0055152
C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, S. Bensalem, David Probst, Property preserving abstractions for the verification of concurrent systems computer aided verification. ,vol. 6, pp. 11- 44 ,(1995) , 10.1007/BF01384313
Patrick Cousot, Radhia Cousot, Abstract interpretation Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '77. pp. 238- 252 ,(1977) , 10.1145/512950.512973
Edmund M. Clarke, Orna Grumberg, David E. Long, Model checking and abstraction ACM Transactions on Programming Languages and Systems. ,vol. 16, pp. 1512- 1542 ,(1994) , 10.1145/186025.186051
Dennis Dams, Rob Gerth, Orna Grumberg, Abstract interpretation of reactive systems ACM Transactions on Programming Languages and Systems. ,vol. 19, pp. 253- 291 ,(1997) , 10.1145/244795.244800
Abelardo Pardo, Gary D. Hachtel, Automatic Abstraction Techniques for Propositional µ-calculus Model Checking computer aided verification. pp. 12- 23 ,(1997) , 10.1007/3-540-63166-6_5
T. E. Uribe, M. A. Colon, Generating finite-state abstractions of reactive systems using decision procedures Lecture Notes in Computer Science. pp. 293- 304 ,(1998)