Code Mutation in Verification and Automatic Code Correction

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

@InProceedings{DBLP:conf/tacas/KatzP10,

• author = "Gal Katz and Doron Peled",
• title = "Code Mutation in Verification and Automatic Code Correction",
• booktitle = "16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010",
• 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, http://dblp.uni-trier.de",
• 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

Citations