Caveat is a purely static analysis tool for the C language, devoted to embedded applications. Caveat ( was developed by the Research Centre of CEA (French Nuclear Energy Agency). It contains a predicates language, a VC generator, and a proof tool to discharge them. For each function, the tool computes a weakest precondition based on some pre- and post-conditions. The advantage of the Hoare method is to give an exact result of the possibility of such errors occurring. The drawback is that it is sometimes necessary to provide loop invariants as well as hypotheses and additional information manually for trying to prove the presence or absence of errors. This makes the process interactive but allows you to understand the errors origins. Caveat is used by Airbus Industries.

Was this article helpful?

0 0
The Ultimate Computer Repair Guide

The Ultimate Computer Repair Guide

Read how to maintain and repair any desktop and laptop computer. This Ebook has articles with photos and videos that show detailed step by step pc repair and maintenance procedures. There are many links to online videos that explain how you can build, maintain, speed up, clean, and repair your computer yourself. Put the money that you were going to pay the PC Tech in your own pocket.

Get My Free Ebook

Post a comment