LTL properties in bounded model checking via assertions
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) -&gt; 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).