We present MCGP -- a tool for generating and correcting code, based on our synthesis approach combining deep Model Checking and Genetic Programming. Given an LTL specification, genetic programming is used for generating new candidate solutions, while deep model checking is used for calculating to what extent (i.e., not only whether) a candidate solution program satisfies a property. The main challenge is to construct from the result of the deep model checking a fitness function that has a good correlation with the distance of the candidate program from a correct solution. The tool allows the user to control various parameters, such as the syntactic building blocks, the structure of the programs, and the fitness function, and to follow their effect on the convergence of the synthesis process.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Uy, Nguyen Quang; Hoai, Nguyen Xuan; O’Neill, Michael; McKay, R.I.; Phong, Dao Ngoc: On the roles of semantic locality of crossover in genetic programming (2013)
- Graf, Susanne; Peled, Doron; Quinton, Sophie: Achieving distributed control through model checking (2012)
- He, Pei; Kang, LiShan; Johnson, Colin G.; Ying, Shi: Hoare logic-based genetic programming (2011)
- Katz, Gal; Peled, Doron: Code mutation in verification and automatic code correction (2010)
- Katz, Gal; Peled, Doron: MCGP: a software synthesis tool based on model checking and genetic programming (2010)
- Katz, Gal; Peled, Doron: Genetic programming and model checking: Synthesizing new mutual exclusion algorithms (2008)