Abstract

Many formal methods tools exist that can assist in the creation of correct software programs, and more are created each year. Yet many of these tools focus only on one specific technique, and are unable to deal with problems that are unsuited for that technique. We believe that combining tools that implement different techniques can yield great results. Yet it seems that little research is being done in this area. We suspect that one of the reasons is that formal methods tools tend to be hard to integrate with existing software. If integrating different formal methods tools were easier, then the barrier to combine different tools would be much lower. As a secondary effect, when tools are easier to integrate it will be easier for them to be adopted outside the academic world. In this thesis we will explore the difficulty of integrating different formal methods tools by performing a case study in which we will create a framework for generating loop invariants for Java programs. The tools for generating loop invariants will serve as a hopefully representative sample of formal methods tools in general. The framework will integrate several existing tools that either perform automated loop invariant generation or contribute to automated loop invariant generation. We will report on the problems encountered during the integration of the different tools and investigate how these problems could have been avoided. Based on this analysis we will create guidelines that can be used by formal methods researchers to make the results of their work more accessible to others. The ultimate aim of these guidelines is twofold: to facilitate research by making it easier for formal methods researchers to build on the work of others, and to allow research results to make the jump from the academic world into the software development industry.

Additional Resources

1. final report