| Solving Software Reuse Problems with Theorem Provers (2007) | |||||||||||||||
Abstract | |||||||||||||||
| In NORA/HAMMR, we investigate the application of automated theorem provers to retrieve software components based on their formal specifications. The problem pro le has major impacts on the problem solving process and integration and preprocessing steps, e.g., simplification, become as important as the actual proving process. NORA/HAMMR thus uses a pipeline of filters of increasing deductive strength. Only in the final filter provers are applied. Here, we use ILF to control competition between different systems. Experiments confirm this approach. With moderate timeouts we already achieve an overall recall of approximately 80%. | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||