Multiple abstraction refinement in symbolic model checking
Abstract
Tóm tắt
Article Details
References
Brin, Sergey and Page, Lawrence. The anatomy of a largescale hyper-textual Web search engine. InProc. of WWW7, pages 107-117, Brisbane, Australia, 1998.
Clarke E. M., etal. Formal methods: state of the art and future directions. ACM Computing Surveys, 1996.
Clarke E. M., Grumberg O., and Peled D. A., Model Checking, MIT Press, 1999
Clarke E. M., Grumberg O., Jha S., Lu Y., and Veith H., Counter-example-Guided Abstraction Refinement, CAV'00, LNCS, vol. 1855, pp. 154-169, 2000.
Dennis Dams: Abstraction in Software Model Checking: Principles and Practice (Tutorial Overview and Bibliography). SPIN 2002: 14-21.
Edelkamp S., Lluch-Lafuente A., and Leue S., Directed Explicit Model Checking with HSF-SPIN, SPIN'01, LNCS, vol. 2057, pp. 57-79, 2001.
Fei He, Xiaoyu Song, William N.N. Hung, Ming Gu, Jiaguang Sun, "Integrating Evolutionary Computation with Abstraction Refinement for Model Checking,"IEEE Transactions on Computers, vol. 59, no. 1, pp. 116-126, Jan. 2010, doi:10.1109/TC.2009.105.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. 1992. Symbolic model checking: 1020 states and beyond. Inf. Comput. 98, 2 (June 1992), 142-170.
Menzies T., Owen, D., and Richardson J., The Strangest Thing about Software, IEEE Computer, vol. 40, no. 1, pp. 54-60, 2007.
Pelanek R., Typical structural properties of state spaces, LNCS, vol. 2989, pp. 5-22, 2004.
Qian K., Nymeyer A., Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases, TACAS'04, LNCS, vol. 2988, pp. 497-511, 2004.
Qian K., Nymeyer A., Abstraction-guided model checking using symbolic IDA* and heuristic synthesis, FORTE'05, LNCS, vol. 3731, pp. 275-289, 2005.
Qian K., Nymeyer A, and Susanto S.. Experiments with Multiple Abstraction Heuristics in Symbolic Verification, SARA 2005, LNAI 3607, pp. 290-304, 2005.
Qing Cui, Alex Dekhtyar., On Improving Local Website Search Using Web Server Traffic Logs: A Preliminary Report, 2005.
Thang. H. Bui, Nymeyer A., Formal Verification Based on Guided Random Walks, iFM'09, LNCS, vol. 5423, pp. 72-87, 2009a.
Thang. H. Bui, Nymeyer A., Formal Model Simulation: Can it be Guided?, SSBSE'09, pp. 93-96, IEEE CS, 2009b.
Thang. H. Bui, Nymeyer A., Heuristic Sensitivity in Guided Random-Walk Based Model Checking, SEFM'09, pp. 125-134, IEEE CS, 2009c.
Thang. H. Bui, Phuong. B.K. Dang, Yet another variable dependency analysis for abstraction guided model checking, SEATUC 2012.
Thang. H. Bui, Phan. T. H. Nguyen, Convergent Propagtion variable dependency analysis for multiple abstraction model checking, SEATUC 2013.
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre.Lazy Abstraction. In ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, pages 58-70, 2002.