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
#include <pthread.h>
int a = 0;
void * f(void * x)
{
a = 1;
return x;
}
int main()
{
pthread_t t;
pthread_create(&t, 0, f, 0);
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.