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

Application domain/field

Type of tool

Synthesis tool

Expected input

Expected output

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


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


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

Related papers

Last publication date

18 July 2018

Related tools

compared to Blaze

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.