Institute of Information Science, Academia Sinica



Press Ctrl+P to print from browser


Automatic Construction of Code using Genetic Programming and Model Checking

  • LecturerDr. Doron Peled (Bar Ilan University)
    Host: Dr. Tyng-Ruey Chuang
  • Time2010-08-23 (Mon.) 14:00 – 15:00
  • LocationAuditorium 106 at new IIS Building
Abstract: About 60% of the investment in Microsoft goes to software testing. Model checking can automatically search for bugs and provide counterexamples to show that the software does not satisfy its specification but is not expected to find all the errors in the code. A more difficult challenge is to construct programs directly from the specification. This is an intractable problem already for sequential code and for concurrent code is undecidable. We propose a new alternative for constructing correct code from its specification using a combination of genetic programming and model checking. The genetic approach applies a heuristic search in the space of programs for an instance that satisfies its specification using the model checking approach. We have applied this technique to various cases, including the automatic generation of code for mutual exclusion, and other examples. We also applied this method to find errors in a complicated protocol with complicated architecture and to correct this protocol. Although this is not likely to replace the job of a programmer, the method is successful in creating code in very intricate and challenging cases that are difficult to program manually. Bio: Research Interests Formal methods, formal veri_cation, model-checking, software testing, software engineering, mathematical logic, automata and formal languages, semantics of programming languages, development and experiments with software analysis systems. Education D.Sc., The Technion, Israel Institute of Science, Department of Computer Science, supervisors: Prof. Shmuel Katz and Prof. Amir Pnueli. Research title: `Veri_cation Methods in Temporal Logics', 1991. M.Sc., The Technion, Israel Institute of Science, Department of Computer Science, supervisor: Prof. Shmuel Katz. Research title: `Interleaving Set Temporal Logic', 1987. B.Sc., cum lauda, The Technion, Israel Institute of Science, Department of Computer Science,1984. Awards and Honors _ President's list 1984. _ Gutwirt Excellency, Technion 1985. _ Full scholarship, 1985{1987. _ EASST (European Association of Software Science and Technology) Best Software Science Paper presented at the European Joint Conference on Theory and Practice of Software (ETAPS) 2001, April 2-6, Genova, Italy.