Technical Report,01 Oct 2014,31 Oct 2018
Kestrel Institute Alto United States
Pagination or Media Count:
This report describes Derivation Miner, an effort under the DARPA Mining and Understanding of Software Enclaves MUSE program. The research team included Kestrel Institute, Kestrel Technology, UT-Austin, and Qadium. The team investigated the question of whether large online repositories of open source computer code could be used to assist program synthesis in such a way that the result has high assurance. The results of the effort show that this is indeed possible. A variety of indexing, analysis, and search tools have been developed and it has been demonstrated, in many cases, that these tools can be used to identify code in the MUSE corpus that has the desired functionality. Formal proof tools have also been developed, including the Automated Program Transformation APT and Axe toolkits, which have been demonstrated over many examples, verifying code found in the wild can be used to synthesize proven programs.
- Computer Programming and Software