AUFOVER: The Automation of Formal Verification

The Automation of Formal Verification (AUFOVER) project responds to the ever-growing need for rapid and high-quality software verification that is carried out within the development life cycle. In the recent years, the university partners of the project have developed, on the basis of formal mathematical methods, an innovative way of verification, which the industrial partners (Honeywell and Red Hat) have shown interest in, in terms of its integration into their verification processes, with the aim of automatically detecting errors that are currently being detected only manually. This project should contribute to establishing efficient collaboration between universities and industrial partners, who will also act as application guarantors and will be able to reliably evaluate the expected benefits of the project findings and outputs, including the quantification of savings achieved.

The goal of the Automation of Formal Verification (AUFOVER) project is to develop automated formal verification tools and integrate them for industrial use. The tools to be developed or improved within the projects are Verification Server, Verification Server Client Application, csmock plug-ins, DIVINE, Symbiotic and Testos. The purpose of the grant is to finish the development of university tools based on formal mathematical methods and their transfer to a commercial environment, including integration with industrial partners’ tools and incorporation of these tools into the commercial processes for software verification.