Synthesis of Logic Interpretation
Jian Xiang, John Knight, and Kevin Sullivan
Proceedings of the 18th IEEE Symposium on High Assurance Systems Engineering, (HASE),  2017.
Abstract.

Logic interpretations define the relationships between real-world entities and their logic representations. We introduce an explicit structure for documenting interpretations based on real-world types. As we have demonstrated previously, the benefits of using real-world types can be considerable, but the effort required might deter programmers. In this paper, we introduce a semi-automated mechanism that: (a) synthesizes candidate real-world types, (b) infers real-world type bindings for program variables, and (c) synthesizes candidate type rules from verified or trusted programs. We illustrate the synthesis approach using an open-source project for which we have previously developed a complete real-world type system.