Model Checking for AlphaCode-Generated Programs

AlphaCode (AC) can generate C++ programs automatically. However, the properties of the programs need to be verified. It is an open challenge to complete the task automatically using the model checking technique. To deal with this issue, a novel approach is proposed in this study. First, a program generated by AlphaCode is modeled using a formal mechanism, such as automata or graphs. Second, a property that needs to be satisfied in states and paths of the program can be described by a logic formula, especially for a temporal logic one. On the basis of it, the model checking problem for AC-generated programs is transformed to a common model checking one. A case study on using of bounded model checker for AC-generated programs demonstrates the feasibility of the proposed method.