PV2 ⊧ ATLAS: AuTomated Learning of AbStractionslearns abstractions and transformers from a language and a set of synthesis problems

Application domain/field

• Program synthesis
• Abstraction-Guided Synthesis (AGS)

Type of tool

Synthesis tool

Expected input

• DSL
• Abstraction-Guided Synthesizer (AGS)
• Training set of synthesis problems (i.e. input-output problems)

Expected output

Abstract domain in the form of predicate templates and abstract transformers for each DSL construct.

Internals

Tree interpolation, data-driven constraint solving Uses Z3, JLinAlg

Comments

"a novel technique for automatically learning domain-specific abstractions that are useful for instantiating an example-guided synthesis framework in a new domain"