2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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]"? $\endgroup$ – Raphael Nov 7 '15 at 10:55
  • 1
    $\begingroup$ 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. $\endgroup$ – Klaus Draeger Nov 7 '15 at 11:20
  • $\begingroup$ I generalized the formulation a little. $\endgroup$ – Markus Müller Nov 7 '15 at 12:16
  • $\begingroup$ 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? $\endgroup$ – ivcha Aug 29 '16 at 20:47
2
$\begingroup$

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).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.