A query regarding CPAChecker

[Omar bataineh]

Hi,

We attempt to improve/refine an initial set of invariants generated for a loop L using the CPAChecker. We assume we have a starting collection of dynamically generated invariants  (In_1,..., In_n). Can we apply reachability analysis techniques for this specific task by checking, for instance, the following reachability property?
 G (L.F => (In_1 /... /In_n)), where F is the collection of program L's final/halting locations and G is the global temporal operator.

What is the most effective way to generate or refine program invariants with CPAChecker? 

Thank you in advance.

[Philipp Wendler]

Dear Omar,

thank you for your interest in CPAchecker.

Am 20.08.23 um 20:09 schrieb Omar bataineh:

> We attempt to improve/refine an initial set of invariants generated for a
> loop L using the CPAChecker. We assume we have a starting collection of
> dynamically generated invariants (In_1,..., In_n). Can we apply
> reachability analysis techniques for this specific task by checking, for
> instance, the following reachability property?
> G (L.F => (In_1 /... /In_n)), where F is the collection of program L's
> final/halting locations and G is the global temporal operator.

This would be equivalent to simply asserting the invariants whenever the
program exits, right? So yes, this would be possible and the easiest way
is usually to just add these asserts.

> What is the most effective way to generate or refine program invariants
> with CPAChecker?

This question is quite broad and it depends somewhat on what you want to
do. We have for example one analysis that does not find 1-inductive
invariants, but k-inductive invariants (for some k), is this enough?

1-inductive invariants are produced for example by our configuration
using predicate abstraction, i.e. "-predicateAnalysis".
This will provide invariants in output/invariants.txt

Greetings
Philipp

--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181

[Omar bataineh]

Thank you, Philipp, for your response. 

We intend to use CPAChecker to compute invariants for faulty programs that might crash at specific locations. Assume that program P may crash at location l_f. Assume als that location l_h is a halting location where the program terminates normally.  Can we create reachability queries to compute invariants at locations l_h (successful runs) and l_f (faulty runs)? Can we model crash events in the query?

Omar

--
You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cpachecker-users/af320e89-81e8-a9ff-ab33-2dddee69adc3%40philippwendler.de.

[Philipp Wendler]

Dear Omar,

Am 29.08.23 um 14:28 schrieb Omar bataineh:

> We intend to use CPAChecker to compute invariants for faulty programs that
> might crash at specific locations. Assume that program P may crash at
> location l_f. Assume als that location l_h is a halting location where the
> program terminates normally. Can we create reachability queries to compute
> invariants at locations l_h (successful runs) and l_f (faulty runs)? Can we
> model crash events in the query?

Hm, this depends somewhat on what kind of invariants do you want.

Typically, the goal of a verifier is to compute invariants that are
overapproximations but strong enough to prove a certain property.
However, once the program has reached l_h, l_f is trivially unreachable,
so the invariant that you would get for l_h would likely be just "true".

An overapproximation of the reachable states at l_f is not something
that we typically ask a verifier to produce, we want an
underapproximation that proves that l_f is reachable. Again, no
invariant at l_f is necessary for the verifier to prove something, so it
would not compute something stronger than "true".

So what kind of invariant do you want?

[Omar bataineh]

Thanks Philipp for the explanation. 

For the purpose of program repair, we would like to construct invariants on the program's variables at both the faulty location and the halting location. The goal is to identify violating invariants that need to be repaired and desired invariants that need to be preserved when repairing the program. We assume that l_f stands for a statement that stops the program and that l_f stands for a statement that occasionally causes the program to crash.

Omar

--
You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/cpachecker-users/ab532471-de8f-d39b-8c4c-07fbf8da7391%40philippwendler.de.

[Philipp Wendler]

Hi Omar,

Am 04.09.23 um 14:35 schrieb Omar bataineh:

> For the purpose of program repair, we would like to construct invariants on
> the program's variables at both the faulty location and the halting
> location. The goal is to identify violating invariants that need to be
> repaired and desired invariants that need to be preserved when repairing
> the program.

Well, "true" is a valid invariant at any location. Of course, it is a
useless invariant, but it is one. So if you just ask an invariant
generator "give me some invariant for location l", what would prevent it
from always returning "true"?

To solve this, one needs to know what distinguishes a useful invariant
from a useless invariant for you. What properties should your invariant
fulfill? For example, for the purpose of proving program safety we ask
for invariants that are inductive and strong enough to prove some
specific property. Then the invariant generator is (typically) forced to
provide some non-trivial invariants.

With this information it would be possible to start thinking about
whether and how CPAchecker can produce them.