Introduction to CEGIS

Notes about counter example guided inductive programsynthesis
program-synthesis
CEGIS
introduction
Published

April 6, 2023

Counter Example Guided Inductive Synthesis (CEGIS)

In CEGIS, with a supplied specification, a synthesiser produces a program that may satisfy the specification, and a verifier determines if this is true, otherwise it will provide a defined form of feedback to the synthesiser to further guide its search. The feedback is usually a counterexample - an input upon which the program did not satisfy the specification.

References

[^1] A. Solar-Lezama, MIT 6.S981 Introduction to Program Synthesis [^2] J. Bornholt 2015 Program Synthesis Explained