- author = "Gal Katz and Doron Peled",
- title = "Synthesis of Parametric Programs using Genetic Programming and Model Checking",
- title2 = "Tutorial on Synthesis of Parametric Programs using Genetic Programming and Model Checking",
- booktitle = "Proceedings 15th International Workshop on Verification of Infinite-State Systems",
- year = "2013",
- editor = "Lorenzo Clemente and Lukas Holik",
- series = "EPTCS",
- volume = "140",
- pages = "70--84",
- address = "Hanoi, Vietnam",
- month = "14 " # oct,
- note = "Invited talk",
- keywords = "genetic algorithms, genetic programming",
-
URL = "
http://www.fit.vutbr.cz/~holik/INFINITY13/",
-
URL = "http://dx.doi.org/10.4204/EPTCS.140.5",
-
URL = "http://dx.doi.org/10.4204/EPTCS.140",
- bibsource = "DBLP, http://dblp.uni-trier.de",
- size = "15 pages",
- abstract = "We show how the use of genetic programming, in combination of model checking and testing, provides a powerful way to synthesise programs. Whereas classical algorithmic synthesis provides alarming high complexity and undecidability results, the genetic approach provides a surprisingly successful heuristics. We describe several versions of a method for synthesising sequential and concurrent systems. To cope with the constraints of model checking and of theorem proving, we combine such exhaustive verification methods with testing. We show several examples where we used our approach to synthesise, improve and correct code.",
- arxiv_abstract = "Formal methods apply algorithms based on mathematical principles to enhance the reliability of systems. It would only be natural to try to progress from verification, model checking or testing a system against its formal specification into constructing it automatically. Classical algorithmic synthesis theory provides interesting algorithms but also alarming high complexity and undecidability results. The use of genetic programming, in combination of model checking and testing, provides a powerful heuristic to synthesise programs. The method is not completely automatic, as it is fine tuned by a user that sets up the specification and parameters. It also does not guarantee to always succeed and converge towards a solution that satisfies all the required properties. However, we applied it successfully on quite nontrivial examples and managed to find solutions to hard programming challenges, as well as to improve and to correct code. We describe here several versions of our method for synthesising sequential and concurrent systems.",
-
notes = "Satellite event of ATVA'13 arXiv.org appears not to be
identical to INFINITY13 hence two abstracts
etc.
http://www.fit.vutbr.cz/~holik/INFINITY13/",
