An Iterative Approach to Language Containment
作者： Felice Balarin , Alberto L. Sangiovanni-Vincentelli
关键词: Heuristic 、 Abstraction (linguistics) 、 Theoretical computer science 、 Containment (computer programming) 、 Boolean function 、 Computation 、 Formal verification 、 Computer science 、 Series (mathematics) 、 Refinement
摘要: We propose an iterative approach to formal verification by language containment. start with some initial abstraction and then iteratively refine it, guided the failure report from tool. show that procedure will terminate, a series of heuristic aimed at reducing size BDD's used in computation, formulate several open problems could improve efficiency procedure. Finally, we present discuss experimental results.
springer.com
sci-hub.st 参考文章(6)
Ramin Hojati, Herve Touati, Robert P. Kurshan, Robert K. Brayton, Efficient ω-regular language containment computer aided verification. pp. 396- 409 ,(1992) , 10.1007/3-540-56496-9_31
S. Bensalem, A. Bouajjani, C. Loiseaux, J. Sifakis, Property Preserving Simulations computer aided verification. pp. 260- 273 ,(1992) , 10.1007/3-540-56496-9_21
R. P. Kurshan, Analysis of Discrete Event Coordination rex workshop on stepwise refinement of distributed systems models formalisms correctness. pp. 414- 453 ,(1989) , 10.1007/3-540-52559-9_74
R. P. Kurshan, K. McMillan, A structural induction theorem for processes Proceedings of the eighth annual ACM Symposium on Principles of distributed computing - PODC '89. pp. 239- 247 ,(1989) , 10.1145/72981.72998
Edmund M. Clarke, Orna Grumberg, David E. Long, Model checking and abstraction symposium on principles of programming languages. pp. 343- 354 ,(1992) , 10.1145/143165.143235
J. R. Burch, E. M. Clarke, K. L. McMillan, David L. Dill, Sequential circuit verification using symbolic model checking Conference proceedings on 27th ACM/IEEE design automation conference - DAC '90. pp. 46- 51 ,(1990) , 10.1145/123186.123223