Abstract
In this paper we use a genetic algorithm to verify safety properties of C programs. We define a new method for program modeling: A Separation Modeling Approach: ASMA, in which programs are represented by two components: Data Model DM, and Control Model CM. The safety verification problem is expressed by means of reachability of some erroneous location L in the program. First, we compute the “Access chain” of L: a string where each position represents the required value of CM elements guards to reach L. Then, the genetic algorithm starts by generating each time a new population which tries to provide an execution which is "conform" to the Access chain. An individual of the population is a set of intervals each one representing an input variable. Our technique allows handling programs containing pointers and function calls.
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.
Similar content being viewed by others
References
Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL, pp. 1–3. ACM, New York (2002)
Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking of C. Tech.Rep.MSR-TR-2001-21, Microsoft Research (2002)
Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Trans. Softw. Eng. 30(6), 388–402 (2004)
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., Grumber, O., Peled, D.: Model Checking. MIT, Cambridge (1999)
Clarke, E.M., Kroening, D., Sharygina, N., Yorav, K.: SatAbs: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Pasareanu, C., Robby, L.S., Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Proc. ICSE, pp. 439–448. ACM, New York (2000)
Cousot, P., Cousot, R.: Abstract interpretation: A Unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principales of Programming Languages, POPL 1977, pp. 238–252 (1977)
Dijkstra, E.: A discipline of programming. Prentice Hall, Englewood Cliffs (1976)
Beyer, D., Henzinger, T.A., Jhala, R., Majumda, R.: The software model cheker Blast. Int. J. Softw. Tools Technol. Transfer (2007)
Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 489–503. Springer, Heidelberg (2006)
Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proc. POPL, pp. 174–186. ACM, New York (1997)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. STTT 2(4), 366–381 (2000)
Hao, J.K.: Memetic algorithms. A book chapter
Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 526–538. Springer, Heidelberg (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.A.: Extreme model checking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 332–358. Springer, Heidelberg (2004)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. POPL, pp. 58–70. ACM, New York (2002)
Holland, J.: Adaptation in natural and artificial systems. The University of Michigan Press, Ann Arbor (1975)
Holzmann, G.J.: The Spin model checker. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)
Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F- Soft: Software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 301–306. Springer, Heidelberg (2005)
Kroening, D., Groce, A., Clarke, E.M.: Counterexample guided abstraction refinement via program execution. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 224–238. Springer, Heidelberg (2004)
Young, M., Pezze, M.: Software Testing and Analysis: Process, Principles and Techniques. Wiley, New York (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aleb, N., Tamen, Z., Kamel, N. (2011). An Evolutionary Approach for Program Model Checking. In: Bellatreche, L., Mota Pinto, F. (eds) Model and Data Engineering. MEDI 2011. Lecture Notes in Computer Science, vol 6918. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24443-8_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-24443-8_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24442-1
Online ISBN: 978-3-642-24443-8
eBook Packages: Computer ScienceComputer Science (R0)