Synthesising Programs with Non-trivial Constants

Area of Science:

• Computer Science
• Software Engineering
• Artificial Intelligence

Background:

• Program synthesis aims to automate software construction.
• Current methods struggle with generating programs containing non-trivial constants.
• Existing tools often require user-defined syntactic restrictions, limiting flexibility.

Purpose of the Study:

• To develop a more efficient program synthesis method for generating programs with non-trivial constants.
• To enhance automated software construction by overcoming limitations of existing techniques.
• To explore the integration of counterexample-guided inductive synthesis with theory solving.

Main Methods:

• Proposed a new approach named CEGIS($$), integrating counterexample-guided inductive synthesis with first-order theory solvers.
• Developed two exemplars of CEGIS($$): one using Fourier-Motzkin (FM) variable elimination and another based on first-order satisfiability.
• Integrated the CEGIS($$) approach into the CVC4 synthesizer.

Main Results:

• CEGIS($$) efficiently explores the solution space for program synthesis without user-guided syntactic restrictions.
• Successfully synthesized programs for a range of intricate benchmarks.
• Demonstrated improved performance when CEGIS($$) was integrated into the CVC4 synthesizer.

Conclusions:

• CEGIS($$) offers a powerful and efficient method for synthesizing programs with non-trivial constants.
• The approach enhances automated software generation capabilities.
• Integration with existing tools like CVC4 yields significant performance benefits.