Code Mutation in Verification and Automatic Code Correction

Created by W.Langdon from gp-bibliography.bib Revision:1.4420

  author =       "Gal Katz and Doron Peled",
  title =        "Code Mutation in Verification and Automatic Code
  booktitle =    "16th International Conference on Tools and Algorithms
                 for the Construction and Analysis of Systems, TACAS
  year =         "2010",
  editor =       "Javier Esparza and Rupak Majumdar",
  publisher =    "Springer",
  series =       "Lecture Notes in Computer Science",
  volume =       "6015",
  pages =        "435--450",
  address =      "Paphos, Cyprus",
  month =        "20-28 " # mar,
  keywords =     "genetic algorithms, genetic programming, SBSE",
  isbn13 =       "978-3-642-12001-5",
  DOI =          "doi:10.1007/978-3-642-12002-2_36",
  size =         "16 pages",
  bibsource =    "DBLP,",
  abstract =     "Model checking can be applied to finite state systems
                 in order to find counterexamples showing that they do
                 not satisfy their specification. This was generalized
                 to handle parametric systems under some given
                 constraints, usually using some inductive argument.
                 However, even in the restricted cases where these
                 parametric methods apply, the assumption is usually of
                 a simple fixed architecture, e.g., a ring. We consider
                 the case of nontrivial architectures for communication
                 protocols, for example, achieving a multi party
                 interaction between arbitrary subsets of processes. In
                 this case, an error may manifest itself only under some
                 particular architectures and interactions, and under
                 some specific values of parameters. We apply here our
                 model checking based genetic programming approach for
                 achieving a dual task: finding an instance of a
                 protocol which is suspicious of being bogus, and
                 automatically correcting the error. The synthesis tool
                 we constructed is capable of generating various
                 mutations of the code. Moving between them is guided by
                 model checking analysis. In the case of searching for
                 errors, we mutate only the architecture and related
                 parameters, and in the case of fixing the error, we
                 mutate the code further in order to search for a
                 corrected version. As a running example, we use a
                 realistic nontrivial protocol for multiparty
                 interaction. This protocol, published in a conference
                 and a journal, is used as a building block for various
                 systems. Our analysis shows this protocol to be, as we
                 suspected, erroneous; specifically, the protocol can
                 reach a livelock situation, where some processes do not
                 progress towards achieving their interactions. As a
                 side effect of our experiment, we provide a correction
                 for this important protocol obtained through our
                 genetic process.",
  notes =        "Held as Part of the Joint European Conferences on
                 Theory and Practice of Software, ETAPS 2010",

Genetic Programming entries for Gal Katz Doron A Peled