×

zbMATH — the first resource for mathematics

Hoare logic-based genetic programming. (English) Zbl 1219.68144
Summary: Almost all existing genetic programming systems deal with fitness evaluation solely by testing. In this paper, by contrast, we present an original approach that combines genetic programming with Hoare logic with the aid of model checking and finite state automata, henceby proposing a brand new verification-focused formal genetic programming system that makes it possible to evolve reliable programs with mathematically verified properties.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68T27 Logic in artificial intelligence
Software:
MCGP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Rich C, Waters R C. Automatic programming: myths and prospects. Computer, 1988, 21: 40–51 · Zbl 05089900 · doi:10.1109/2.75
[2] Koza J R. Genetic Programming: On the Programming of Computers by Means of Natural Selection. Cambridge, MA: The MIT Press, 1992 · Zbl 0850.68161
[3] Holland J H. Adaptation in Natural and Artificial Systems. Michigan: The University of Michigan Press, 1975
[4] Mitchell M. An Introduction to Genetic Algorithms. Cambridge: MIT Press, 1996 · Zbl 0906.68113
[5] Oltean M, Grosan C. A comparison of several linear genetic programming techniques. Complex Syst, 2004, 14: 1–29 · Zbl 1167.90695
[6] Abraham A, Nedjah N, de Macedo M L. Evolutionary computation: from genetic algorithms to genetic programming. In: Nedjah N, et al., eds. Studies in Computational Intelligence. Berlin: Springer-Verlag, 2006. 1–20
[7] Koza J R. Human-competitive machine intelligence by means of genetic algorithms. In: Booker L, Forrest S, Mitchell M, et al., eds. Perspectives on Adaptation in Natural and Artificial System. Oxford: Oxford University Press, 2005. 33–55
[8] Koza J R, Bennett F H III, Andre D, et al. Four problems for which a computer program evolved by genetic programming is competitive with human performance. In: Proceedings of IEEE International Confer. on Evolutionary Computation, Nagoya, Japan, 1996. 1–10
[9] Koza J R, Keane M A, Yu J, et al. Automatic creation of human-competitive programs and controllers by means of genetic programming. Genet Program Evolv Mach, 2000, 1: 121–164 · Zbl 1006.68632 · doi:10.1023/A:1010076532029
[10] Binard F, Felty A. An abstraction-based genetic programming system. In: GECCO’ 2007, London, UK, 2007. 2415–2422
[11] Frias-Martinez E, Gobet F. Automatic generation of cognitive theories using genetic programming. Minds Mach, 2007, 17: 287–309 · Zbl 05349510 · doi:10.1007/s11023-007-9070-6
[12] O’Neill M, Ryan C. Grammatical evolution. IEEE Trans Evol Comput, 2001, 5: 349–358 · Zbl 05452034 · doi:10.1109/4235.942529
[13] Sette S, Boullart L. Genetic programming: principles and applications. Eng Appl Artif Intell, 2001, 14: 727–736 · doi:10.1016/S0952-1976(02)00013-1
[14] Montana D J. Strongly typed genetic programming. Evol Comput, 1995, 3: 199–230 · Zbl 05412779 · doi:10.1162/evco.1995.3.2.199
[15] Koza J R. Genetic Programming II: Automatic Discovery of Reusable Programs. Cambridge, MA: MIT Press, 1994 · Zbl 0850.68160
[16] Wang M L, Leung K S. Data Mining Using Grammar Based Genetic Programming and Applications. Dordrecht: Kluwer Academic Publishers, 2002. 27–99
[17] Johnson C G. Genetic programming with fitness based on model checking. In: Ebner M, et al. eds. EuroGP 2007. Genetic Programming, LNCS 4445. Berlin: Springer-Verlag, 2007. 114–124
[18] He P, Kang L S, Fu M. Formality based genetic programming. In: Proc. of IEEE Congress on Evolutionary Computation. Hong Kong. 2008. 4081–4088
[19] Katz G, Peled D. Model checking-based genetic programming with an application to mutual exclusion. In: Ramakrishnan C R, Rehof J, eds. TACAS2008, LNCS 4963, Budapest, Hungary, 2008. 141–156 · Zbl 1134.68411
[20] Chen H W, Wang J, Dong W. High confidence software engineering technologies (in Chinese). Acta Electr Sin, 2003, 31: 1933–1938
[21] Dijkstra E W. A Discipline of Programming. Englewood Cliffs, NJ: Prentice-Hall, 1976 · Zbl 0368.68005
[22] Brinksma E. Verification is experimentation. Int J STTT, 2001, 3: 107–111 · Zbl 1002.68587
[23] Kneuper R. Limits of formal methods. Form Aspects Comput, 1997, 9: 379–394 · doi:10.1007/BF01211297
[24] Clarke E M, Wing J M, et al. Formal methods: state of the art and future directions. ACM Comput Surv, 1996, 28: 626–643 · doi:10.1145/242223.242257
[25] Huth M, Ryan M. Logic in Computer Science: Modelling and Reasoning about System. Cambridge: Cambridge University Press, 2004 · Zbl 1073.68001
[26] Lin H M, Zhang W H. Model checking: theories, techniques, and applications (in Chinese). Acta Electr Sin, 2002, 30: 1907–1912
[27] Visser W, Havelund K, Brat G, et al. Model checking programs. Automat Softw Eng, 2003, 10: 203–232 · Zbl 01904973 · doi:10.1023/A:1022920129859
[28] Hoare C A R. An axiomatic basis for computer programming. CACM, 1969, 12: 576–583 · Zbl 0179.23105 · doi:10.1145/363235.363259
[29] Manna Z. Mathematical theory of partial correctness. J Comput Syst Sci, 1971, 5: 239–253 · Zbl 0215.55905 · doi:10.1016/S0022-0000(71)80035-1
[30] Singh A K, Ghanekar U, Bandyopadhyay A K. Specifying mobile network using a WP-like formal approach. Revista Colomb Comput, 2005, 6: 59–77
[31] Winskel G. The Formal Semantics of Programming Language: An Introduction. Cambridge, Massachusetts: The Mit Press, 1993 · Zbl 0919.68082
[32] Yang F Q, Wang Q X, Mei H, et al. Reuse-based software production technology. Sci China Ser F-Inf Sci, 2001, 44: 8–19 · doi:10.1007/BF02713936
[33] Xiong H M, Ying S, Yu L, et al. A composite reuse of architectural connectors using reflection (in Chinese). J Softw, 2006, 17: 1298–1306 · Zbl 1099.68598 · doi:10.1360/jos171298
[34] Hopcroft J E, Motwani R, Ullman J D. Introduction to Automata Theory, Languages, and Computation. 3rd ed. Upper Saddle River, NJ: Pearson Education Inc., 2007. 1–170 · Zbl 0980.68066
[35] Aho A V, Lam M S, Sethi R, et al. Compilers: Principles, Techniques, and Tools. 2nd ed. Boston, MA: Addison Wesley, 2007 · Zbl 1155.68020
[36] Garey M, Johnson D S. Computers and Intractability-A Guide to the Theory of NP-completeness. San Francisco: Freeman, 1979. 213 · Zbl 0411.68039
[37] Kaner C, Falk J, Nguyen H Q. Testing Computer Software. 2nd ed. New York: John Wiley and Sons, Inc., 1999. 480 · Zbl 0838.68018
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.