Maxime Derri

icon location I'm a PhD student working on the verification of eBPF programs, at Inria and Orange.

Results 3 comments of Maxime Derri

The widening operator causes termination issues

For debugging, you can add a print before and after the extrapolate() function to check that the invariant is bottom.

The widening operator causes termination issues

Hmm I didn't tested this issue

The widening operator causes termination issues

In the issue you mentionned, Alan Jowett said that the verifier hang for 10min and assertions where checked after the invariant computation meaning that the verifier found an invariant? Here...