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.

References in zbMATH (referenced in 15 articles , 1 standard article )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Benouhiba, Toufik: A multi-level refinement approach for structural synthesis of optimal probabilistic models (2021)
  2. Basset, N.; Kwiatkowska, M.; Wiltsche, C.: Compositional strategy synthesis for stochastic games with multiple objectives (2018)
  3. Bloem, Roderick; Chatterjee, Krishnendu; Jobstmann, Barbara: Graph games and reactive synthesis (2018)
  4. Evrard, Hugues; Lang, Frédéric: Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous (2017)
  5. Finkbeiner, Bernd; Olderog, Ernst-Rüdiger: Petri games: synthesis of distributed systems with causal memory (2017)
  6. Chatterjee, Krishnendu; Henzinger, Thomas A.; Jobstmann, Barbara; Singh, Rohit: Measuring and synthesizing systems in probabilistic environments (2015)
  7. 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)
  8. Graf, Susanne; Peled, Doron; Quinton, Sophie: Achieving distributed control through model checking (2012)
  9. He, Pei; Kang, LiShan; Johnson, Colin G.; Ying, Shi: Hoare logic-based genetic programming (2011)
  10. Katz, Gal; Peled, Doron: Synthesizing solutions to the leader election problem using model checking and genetic programming (2011) ioport
  11. Katz, Gal; Peled, Doron; Schewe, Sven: Synthesis of distributed control through knowledge accumulation (2011) ioport
  12. Katz, Gal; Peled, Doron: Code mutation in verification and automatic code correction (2010) ioport
  13. Katz, Gal; Peled, Doron: MCGP: a software synthesis tool based on model checking and genetic programming (2010) ioport
  14. Katz, Gal; Peled, Doron: Genetic programming and model checking: Synthesizing new mutual exclusion algorithms (2008)
  15. Katz, Gal; Peled, Doron: Model checking-based genetic programming with an application to mutual exclusion (2008)