LTL properties in bounded model checking via assertions

Question

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.

Answer 1

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;

proctype thread1() {
  a = 1;
}

init {
  a = 0; 
  end = false;
  run thread1();
  do
  :: (a == 0) -> skip;
  od;
  end = true;
}

ltl prop { always (eventually end) }

The code follows the given C code, where do simulates checking the condition with while loop. When checking if prop holds, SPIN will find an "acceptance cycle" that shows that main might get constantly scheduled for execution and starve thread1, thus refuting the formula. If a "fair" scheduler is assumed (e.g. with enforcing "weak fairness" SPIN reference), the property will be proven correct.

Note that although such (liveness) properties should be supported, by expressing them in LTL (or other logics like CTL), it is not clear how could they be expressible only with assertions (since assertions state something about the state at particular program point).