The goal of the DerivationMiner project
is to reconstruct (i.e. mine)
formal stepwise refinement and abstraction derivations
from large corpora of
programs, specifications, refinements, abstractions, proofs, and related artifacts.
Our approach combines
big data analysis,
static analysis based on abstract interpretation,
verified lifting of programs to logic,
and automated transformations for refinement-based synthesis.
Mining derivations enables existing code to be re-used,
with formally proved assurance,
in the context of correct-by-construction developments.
DerivationMiner explores analysis-by-synthesis,
where traditional program analysis
is combined with synthesis technology
to reconstruct derivations by alternating
top-down steps (synthesis) and bottom-up steps (analysis).