Inference of contracts for auxiliary procedures in programs that use floating-point arithmetic

Having functionally correct code in safety-critical systems is crucial to avoid life-threatening accidents. Formal verification is a tool that can be used to prove that code does what is expected. Currently, there is a large annotation overhead when writing the specifications, called software contracts, that specify the desired behavior of the code. To help make formal verification more usable for large code bases, like those present in the industry, contract inference has been developed. Contract inference is the concept of automatically generating contracts for auxiliary functions. A formal verification tool containing a contract inference toolchain for C programs called AutoDeduct has been developed. It currently lacks support for floating-point arithmetic, a feature that industry code utilizes. This thesis aims to add the final steps to enable this support. The work focuses on translating the output from the model checker TriCera so that this output can be interpreted as contracts even for programs containing floating point arithmetic. The core challenge is to identify the output patterns and come up with equivalent expressions in the contract language. The translation should also not be a major bottleneck in the performance of the toolchain. To accomplish this, a theoretical translation is proposed. This translation has been implemented into TriCera and evaluated on code examples. The results show that the translation works well, looks to be correct, and is efficient. The implementation was also tested on a template program that was scaled in size with a parameter. The results show that the runtime of the translation scales well to the larger template program. However, not all of the code was able to be fully verified using the generated contracts. Due to time constraints, the reason why this is and what can be done about it is left as future work.