Abstract
The paper presents a novel probabilistic learning approach to state separation problem which occurs in the counterexample guided abstraction refinement. The method is based on the sample learning technique, evolutionary algorithm and effective probabilistic heuristics. Compared with the previous work by the sampling decision tree learning solver, the proposed method outperforms 2 to 4 orders of magnitude faster and the size of the separation set is 76% smaller on average.
This work was supported in part by the Chinese National 973 Plan under grant No. 2004CB719406 and NSF of China under grant No. 60553002.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Clarke, E.M., Gupta, A., Kukula, J.H., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 265–279. Springer, Heidelberg (2002)
Clarke, E., Gupta, A., Strichman, O.: SAT based counterexample-guided abstraction-refinement. IEEE Transactions on Computer Aided Design 23(7), 1113–1123 (2004)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Symposium on Principles of Programming Languages, pp. 58–70 (2002)
Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.Y.: Multiple-counterexample guided iterative abstraction refinement: an industrial evaluation. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 176–191. Springer, Heidelberg (2003)
Gupta, A., Strichman, O.: Abstraction refinement for bounded model checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 112–124. Springer, Heidelberg (2005)
Govindaraju, S.G., Dill, D.L.: Counterexample-guided choice of projections in approximate symbolic model checking. In: ICCAD, pp. 115–119 (2000)
McMillan, K.L., Amla, N.: Automatic abstraction without counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 2–17. Springer, Heidelberg (2003)
Gupta, A., Ganai, M.K., Yang, Z., Ashar, P.: Iterative abstraction using SAT-based BMC with proof analysis. In: ICCAD, pp. 416–423 (2003)
Wang, C., Jin, H., Hachtel, G.D., Somenzi, F.: Refining the SAT decision ordering for bounded model checking. In: DAC, pp. 535–538 (2004)
Dumitrescu, D., Lazzerini, B., Jain, L., Dumitrescu, A.: Evolutionary Computation. CRC Press, Boca Raton (2000)
Beasley, J., Chu, P.: A genetic algorithm for the set covering problem. European Journal of Operational Research 94, 392–404 (1996)
Sen, S.: Minimal cost set covering using probabilistic methods. In: Proceedings of the 1993 ACM/SIGAPP symposium on Applied computing, Indianapolis, Indiana, United States, pp. 157–164. ACM Press, New York (1993)
Aickelin, U.: An indirect genetic algorithm for set covering problems. Journal of the Operational Research Society 53(10), 1118–1126 (2002)
Marchiori, E., Steenbeek, A.: An evolutionary algorithm for large scale set covering problems with application to airline crew scheduling. In: Oates, M.J., Lanzi, P.L., Li, Y., Cagnoni, S., Corne, D.W., Fogarty, T.C., Poli, R., Smith, G.D. (eds.) EvoIASP 2000, EvoWorkshops 2000, EvoFlight 2000, EvoSCONDI 2000, EvoSTIM 2000, EvoTEL 2000, and EvoROB/EvoRobot 2000. LNCS, vol. 1803, pp. 367–381. Springer, Heidelberg (2000)
Syswerda, G.: Uniform crossover in genetic algorithms. In: Proceedings of the 3rd International Conference on Genetic Algorithms, San Mateo, California, USA, pp. 2–9. Morgan Kaufmann Publishers Inc., San Francisco (1989)
Spears, W.M., De Jong, K.A.: On the virtues of parameterized uniform crossover. In: Belew, R., Booker, L. (eds.) Proceedings of the Fourth International Conference on Genetic Algorithms, San Mateo, CA, pp. 230–236. Morgan Kaufman, San Francisco (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
He, F., Song, X., Gu, M., Sun, J. (2006). A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement. In: Graf, S., Zhang, W. (eds) Automated Technology for Verification and Analysis. ATVA 2006. Lecture Notes in Computer Science, vol 4218. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901914_6
Download citation
DOI: https://doi.org/10.1007/11901914_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47237-7
Online ISBN: 978-3-540-47238-4
eBook Packages: Computer ScienceComputer Science (R0)