# LTL properties in bounded model checking via assertions

Is there a way to check LTL properties in a bounded model checker?

As an example, consider a liveness property ($G F p$ - always eventually $p$)? Suppose we have the following trivial program

int a = 0;
void * f(void * x)
{
a = 1;
return x;
}
int main()
{
while (a == 0);
return 1;
}

Is "always eventually main terminates" expressible in a bounded model checker using only assertions?

In principle, you can construct a Büchi automaton from an LTL formula, express it in the modeling language (e.g. as C code) and run it in parallel to the model/program. However, unbounded loops pose a problem to the bounded model checker. Hence, I wonder how such properties can be expressed using assertions, e.g. in CBMC.

• CBMC is a specific software too, I take it? Tool support is offtopic here. Does this reduces to a conceptual question, e.g. of the form "How can I express always-eventually properties in [type of logic]"? Commented Nov 7, 2015 at 10:55
• Essentially, what OP is asking is whether a bounded model checker (like CBMC, cprover.org/cbmc) can be used to check liveness properties like $GFp$ (or possibly CTL properties like $AFp$? It's not quite clear in what sense "always" is used here). Perhaps he could rewrite it along those lines. Commented Nov 7, 2015 at 11:20
• I generalized the formulation a little. Commented Nov 7, 2015 at 12:16
• Was the provided answer helpful and/or useful to you? If not, it would be useful to hear why not, as well as any feedback in general. If yes, can you accept the answer? Commented Aug 29, 2016 at 20:47

The property "always eventually main terminates" should be expressible and verifiable in a bounded model checker. For such properties, the model checker would either verify the property or find a "acceptance cycle" that shows that there exists a loop in an execution trace that does not satisfy the property (by considering execution traces of bounded lengths).

For example, the given property can be expressed in the SPIN model checker with:

int a;
bool end;

a = 1;
}

init {
a = 0;
end = false;