基于遗传编程和模型检验的参数程序综合
Synthesis of Parametric Programs using Genetic Programming and Model Checking
摘要：
形式化方法应用基于数学原理的算法来增强系统的可靠性。尝试从验证、模型检验或根据系统的正式规范测试系统到自动构建系统，这是很自然的。经典的算法综合理论提供了有趣的算法，但也令人震惊的高复杂性和不可判定性的结果。结合模型检验和测试，遗传编程的使用提供了一个强大的启发式综合程序。该方法不是完全自动的，因为它由设置规格和参数的用户进行微调。它也不能保证总是成功并收敛到满足所有所需属性的解决方案。然而，我们成功地将其应用于相当重要的示例，并设法找到解决方案，以应对困难的编程挑战，以及改进和纠正代码。我们在这里描述了几个版本的我们的方法合成顺序和并发系统。
英文摘要：
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 with model checking and testing, provides a powerful heuristic to synthesize 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 synthesizing sequential and concurrent systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
