How to write custom LTL rules to be checked in ESBMC?

[hzyrc6011]

I appreciate this open source project and it really helps me a lot. However, I now have a problem that I still have no idea after looking around documentation, --help arguments, tutorial slides and other issues. My question is described below.

As the following program shown:

int a;

void proc1()
{
a += 1;
}

void proc2()
{
a -= 1;
}

Assume the rule is, a>=-1 in the entire running period, that is, G(a>=-1) in LTL. How could I specify this rule, except adding many assertions below all assignments? Thanks for your help!

[lucasccordeiro]

Hi @hzyrc6011,

Thanks for your interest in using ESBMC.

We researched converting LTL formulae to C monitors via Buechi Automata (cf. https://ssvlab.github.io/lucasccordeiro/papers/sosym2013.pdf). Can I ask you whether you had a chance to read this paper?

Regarding your code, do proc1 and proc2 run infinitely often?

Best, Lucas

[unlimitcc]

Hi @lucasccordeiro , I also have similar problem. If i have a program like this :

/*test.c*/
int a;
void proc1()
{
a = 1;
}

void proc2()
{
a = a + 1;
}

int main(){
a = nondet_int();
proc1();
proc2();
}

then I want to verify this G(a >= 1). I can only find three examples related to LTL in master, but it makes me confused. The verification result is "LTL FAILING", I don't understand what it means.

$ ./ltl2ba -O c -f 'G{a >= 1}' > notltl.c
$ esbmc test.c --ltl notltl.c -DLTL_PREFIX_BOUND=10
ESBMC version 7.6.1 64-bit x86_64 linux
Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc
Parsing test.c
Parsing notltl.c
Converting
Generating GOTO Program
GOTO program creation time: 0.090s
GOTO program processing time: 0.001s
Starting Bounded Model Checking
Symex completed in: 0.000s (52 assignments)
Slicing time: 0.000s (removed 47 assignments)
Generated 14 VCC(s), 3 remaining after simplification (5 assignments)
Checking for LTL_BAD
WARNING: Couldn't find LTL_BAD assertion
Checking for LTL_FAILING
No solver specified; defaulting to z3
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.000s
Solving with solver Z3 v4.8.12
Runtime decision procedure: 0.000s
Found trace satisfying LTL_FAILING
BMC program time: 0.014s
Final lowest outcome: LTL_FAILING

VERIFICATION SUCCESSFUL

There is very little information in the section of the manual about LTL and I don't know exactly what options are available. I wonder if you have any good suggestions or relevant information, Thank you!

[lucasccordeiro]

@fbrausse: could you please assist @unlimitcc?

[lucasccordeiro]

@fbrausse: Can I ask you whether you had a chance to check this issue?