Pervasive formal verification in Verisoft

The Verisoft Project

• Long-term research project to verify software systems
• Funded by the German Federal Ministry of Education and Research
• Applications in, e.g., automotive engineering, security technology, and medical technology

Linking to LEO II using THF

• Identify proof problems in Verisoft on which LEO II performs well
• Generation of proof problems in THF
• Couple Verisoft to LEO II via SystemOnTPTP
• Evaluate efficacy

Win-win-win

• Reduce interaction costs in Verisoft
• Learn limitations of LEO II, to rectify
• Supply THF problems for the TPTP