. "Caveat"@en . "Proof"@en . "WP"@en . "Toolset performance evaluation"@en . "69574c0fba905909775d278f96eb3e0b" . "Denis Favre-Felix" . "Avionics software"@en . "Compiler verification"@en . . "Formal Verification"@en . "Favre-Felix" . "Workbench"@en . "Denis" . "Optimized code generation"@en . "Hoare"@en . "Safety critical systems"@en . "Dijkstra"@en . . "WCET"@en . "Code optimization"@en .