Efficient Detection of Vacuity in ACTL Formulas
作者： Ilan Beer , Shoham Ben-David , Cindy Eisner , Yoav Rodeh
关键词:
摘要: … 2 Actually, if the V operator is derived from the use of the→ operator by the user, we consider the right-hand-side of the original formula to be important even if it is simple. Similarly, we …
springer.com
core.ac.uk
sci-hub.st 参考文章(11)
Ramin Hojati, Robert K. Brayton, Robert P. Kurshan, BDD-Based Debugging Of Design Using Language Containment and Fair CTL computer aided verification. pp. 41- 58 ,(1993) , 10.1007/3-540-56922-7_5
Sérgio Vale Aguiar Campos, Kenneth L. McMillan, Edmund M. Clarke, Vassili Hartonas-Garmhausen, Symbolic Model Checking ,(1993)
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
Edmund M. Clarke, E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic Logic of Programs, Workshop. pp. 52- 71 ,(1981) , 10.1007/BFB0025774
Edmund M. Clarke, David Esley Long, Model checking, abstraction, and compositional verification Carnegie Mellon University. ,(1993)
Orna Grumberg, David E. Long, Model checking and modular verification ACM Transactions on Programming Languages and Systems. ,vol. 16, pp. 843- 871 ,(1994) , 10.1145/177492.177725
E. M. Clarke, O. Grumberg, K. L. McMillan, X. Zhao, Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking design automation conference. pp. 427- 432 ,(1995) , 10.1145/217474.217565
Derek L. Beatty, Randal E. Bryant, Formally Verifying a Microprocessor Using a Simulation Methodology design automation conference. pp. 596- 602 ,(1994) , 10.1145/196244.196575
Ilan Beer, Shoham Ben-David, Cindy Eisner, Avner Landver, RuleBase: an industry-oriented formal verification tool design automation conference. pp. 655- 660 ,(1996) , 10.1145/240518.240642
B. Plessier, C. Pixley, Formal verification of a commercial serial bus interface international phoenix conference on computers and communications. pp. 378- 382 ,(1995) , 10.1109/PCCC.1995.472465