Does CBMC prove termination ?

[Bjarne Corydon]

Hi :)

I've been using CBMC on some real-time embedded code, and I've been wondering about how the successful runs of CBMC on C code relates to termination proofs.

As far as I understand it, CBMC can prove the absence of a lot of run-time exceptions/errors and establish that there is an upper bound on looping - is this correct?

Given the above, does a successful CBMC run with the relevant checks prove that the model/function(s) inspected are guaranteed to terminate? Another way to formulate the question: Assuming absence of run-time errors and unbounded loops and recursion (i.e. "finiteness"), the code inspected can be proved to eventually terminate, right?

The reason I'm asking is that I've been pondering on the checking of safety/liveness properties on my system statically. Since the code is strictly real-time, I don't think I should care much for unbounded liveness other than I think it would give me some hacker-cred if I could boast a claim of termination proof on my code ;)

Regarding safety properties, I think I can check a lot of them through some reachability analysis using CBMC. I haven't thought much about how, but I have stumbled upon the FShell papers.

Please excuse me if I'm abusing either language or terminology, or being unclear. English isn't my native language and I'm not very mature the in the formal computer sciences and the jargon.

Kind regards

/Bjarne

Ps. In my humble opinion CBMC seems perfect for model checking real-time C code, especially if sticking to static allocation, MISRA/JPL-inspired coding style and bounded looping, keep up the good work! :)

[Martin Brain]

On Wed, 2015-04-15 at 15:01 -0700, Bjarne Corydon wrote:
> Hi :)
>
>
> I've been using CBMC on some real-time embedded code, and I've been
> wondering about how the successful runs of CBMC on C code relates to
> termination proofs.
>
>
> As far as I understand it, CBMC can prove the absence of a lot of
> run-time exceptions/errors and establish that there is an upper bound
> on looping - is this correct?

Yes. The run-time errors will be whatever you instrument in
(--bounds-check et al.) and will be reported as an error trace. The
unwinding assertions will tell you if there are traces that hit the
unwinding limit. Thus if CBMC says "VERIFICATION SUCCESSFUL" (and you
haven't disabled the unwinding limits with --no-unwinding-assertions)
you have not only shown that there are no errors but also that all
traces can be described with finite unwindings - i.e. the program
terminates.

> Given the above, does a successful CBMC run with the relevant checks
> prove that the model/function(s) inspected are guaranteed to
> terminate?

Yes, unless you are using --no-unwinding-assertions, which is quite
widely used.

> Another way to formulate the question: Assuming absence of run-time
> errors and unbounded loops and recursion (i.e. "finiteness"), the code
> inspected can be proved to eventually terminate, right?

Yes.

[ A little bit of an aside : the key difference between software
verification and theorem proving is loops / recursion. If they are
unwindable / removeable, etc. then the program can be transformed to a
formula and we can reason about all of it's traces with a prover.
Without unbounded loops / recursion, a program is basically a compact
notation for an expression and these are always guaranteed to terminate.
Loops are what makes this game hard. ]

> The reason I'm asking is that I've been pondering on the checking of
> safety/liveness properties on my system statically. Since the code is
> strictly real-time, I don't think I should care much for unbounded
> liveness other than I think it would give me some hacker-cred if I
> could boast a claim of termination proof on my code ;)

Note that you /can/ prove termination via CBMC but there are also
special purpose tools for just proving termination. One of our
experimental tools for doing this was presented at ESOP yesterday, you
can read about it here:

http://link.springer.com/content/pdf/10.1007/978-3-662-46669-8_8.pdf

I'm not sure if we have a page about the tool just yet but if you're
willing to check out code and compile yourself then we can probably get
you something.

> Regarding safety properties, I think I can check a lot of them through
> some reachability analysis using CBMC. I haven't thought much about
> how, but I have stumbled upon the FShell papers.

FShell is more for test case generation (which you might also be
interested in). For properties, either use the instrumentation options
(run cbmc --help and look at "Program instrumentation options") or write
them in yourself as assert statements if you want to prove functional
properties.

> Please excuse me if I'm abusing either language or terminology, or
> being unclear. English isn't my native language and I'm not very
> mature the in the formal computer sciences and the jargon.

No; that all sounds reasonable to me.

> Ps. In my humble opinion CBMC seems perfect for model checking
> real-time C code, especially if sticking to static allocation,
> MISRA/JPL-inspired coding style and bounded looping, keep up the good
> work! :)

Thank you. Let us know how you get on as we are always interested in
industrial and research applications
( http://www.cprover.org/cbmc/applications.shtml)

Cheers,
- Martin