Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking
作者： E. M. Clarke , O. Grumberg , K. L. McMillan , X. Zhao
关键词: Theoretical computer science 、 Computer Aided Design 、 Computer science 、 Sequential logic 、 Symbolic trajectory evaluation 、 Debugging 、 Programming language 、 Counterexample 、 Model checking 、 TRACE (psycholinguistics)
摘要: Model checking is an automatic technique for verifying sequential circuit designs and protocols. An efficient search procedure used to determine whethe or not the specification satisfied. If it satisfied, our will produce a counter-example execution trace that shows cause of problem. We describe algorithm counter-examples witnesses symbolic model algorithms. This in SMV checker works quite well practice. also discuss how extend more complicated specifications.
acm.org
core.ac.uk
sci-hub.se 参考文章(12)
E. Allen Emerson, Chin Laung Lei, EFFICIENT MODEL CHECKING IN FRAGMENTS OF THE PROPOSITIONAL MU-CALCULUS. logic in computer science. pp. 267- 278 ,(1986)
Robert K. Brayton, Vigyan Singhal, Ramin Hojati, Edge-Streett/ Edge-Rabin Automata Environment for University of California at Berkeley. ,(1994)
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
Kenneth Lauchlin McMillan, Symbolic model checking: an approach to the state explosion problem Ph. D. Thesis, Carnegie Mellon University. ,(1992)
E. M. Clarke, I. A. Browne, R. P. Kurshan, A unified approach for showing language containment and equivalence between various types of Ω-automata colloquium on trees in algebra and programming. pp. 103- 116 ,(1990) , 10.1007/3-540-52590-4_43
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 L Dill, Automatic verification of asynchronous circuits using temporal logic IEE Proceedings E Computers and Digital Techniques. ,vol. 133, pp. 276- 282 ,(1986) , 10.1049/IP-E:19860034
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, Symbolic model checking: 10/sup 20/ states and beyond logic in computer science. ,vol. 98, pp. 142- 170 ,(1990) , 10.1016/0890-5401(92)90017-A
Bryant, Graph-Based Algorithms for Boolean Function Manipulation IEEE Transactions on Computers. ,vol. 35, pp. 677- 691 ,(1986) , 10.1109/TC.1986.1676819