What is ArC?

ArC is a tool for developing formally verified C code for safety-critical and other high-integrity software systems. It works by adapting C and C++ like this:

• First, we subset the language to remove unsafe features, using MISRA-C 2004 as a basis;
• Next, we strengthen the type system to give you the benefits of a strongly-typed language;
• Next, we add preconditions and other constructs to support Verified Design-by-Contract;
• This allows ArC to verify the program using its powerful automatic theorem prover.

All this is done in such a way that your ArC program is still a valid C or C++ program, so that it can be compiled using a standard compiler.

Unlike traditional static analysis tools, ArC not only verifies that your software conforms to the programming language subset, but also gives you mathematical proof that it is free from run-time errors for all possible inputs. You can also use ArC to prove that your software satisfies any safety properties or other functional specifications that you provide. This is clearly preferable to hoping that sufficient data is used during testing to detect all the errors.

ArC uses the same mature automated theorem prover as Perfect Developer. This prover has been developed over many years so that it is able to prove all or nearly all true verification conditions without user intervention.

Interested?

If you would like some more information about ArC, please contact us. And have you seen our blog about verifying C and C++ programs ?