DerivationMiner Project

Team:

• Kestrel Institute (prime)
  • Eric Smith (PI)
  • Alessandro Coglio (Co-PI)
  • Limei Gilham
  • Eric McCarthy
  • James McDonald
  • Eddy Westbrook
• Kestrel Technology
• University of Texas at Austin
• Qadium Inc.

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).