Verifying program with float numbers using z3

[ryanw...@gmail.com]

Hi,

I'm using CPAchecker (the version in "trunk" branch) to verify some program with float numbers and assertions. 

Currently I'm using "-predicateAnalysis" as configuration and "-setprop solver.solver=z3" to set z3 as the backend. But I always get 

Error: Refinement failed: Interpolation failed (theory not supported by interpolation or bad proof)

switching the backend to MATHSAT5 doesn't help, the error becomes "eager fp solver does not support proof generation".

From the post Verifying bubble sort I see I can use "-predicateAnalysis-linear" to approximate the float numbers, but if I set that the verification result is always FALSE even if I remove all the assertions in the source file.

Attached is the source code I'm trying to verify. Thanks.

[Philipp Wendler]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Dear Ryan,

thanks for contacting us!

Am 06.06.2018 um 04:28 schrieb ryanw...@gmail.com:
> I'm using CPAchecker (the version in "trunk" branch) to verify some
> program with float numbers and assertions.
>
> Currently I'm using "-predicateAnalysis" as configuration and
> "-setprop solver.solver=z3" to set z3 as the backend. But I always
> get
>
> Error: Refinement failed: Interpolation failed (theory not
> supported by interpolation or bad proof)

This is a problem of Z3, its interpolation support has several issues.
(And actually, in current Z3 the interpolation was removed completely.)

> switching the backend to MATHSAT5 doesn't help, the error becomes
> "eager fp solver does not support proof generation".

MathSAT unfortunately does not support interpolation that relies on
facts about floats.

So currently there is no real solution for interpolation for floats.
We are implementing a different refinement scheme in CPAchecker that
does not rely on interpolation, but it is not finished yet.

Apart from approximating floats with rationals,
you can also try to verify the program with other approaches that do
not need this kind of interpolation, for example with k-induction
(configuration is "-kInduction") or value analysis (configuration is
"-valueAnalysis").

> From the post Verifying bubble sort

> <https://groups.google.com/forum/#!topic/cpachecker-users/aU8hunUxbpk>

> I see I can use "-predicateAnalysis-linear" to approximate the
> float numbers, but if I set that the verification result is always
> FALSE even if I remove all the assertions in the source file.

This is something I cannot reproduce. If I remove the asserts, I do
not get FALSE.
Please send us the full command line and the exact source you are using.

Greetings, Philipp
- --
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2

iQIcBAEBCAAGBQJbF2huAAoJEGLA94wxqd6Mo7AQAJJRlrJSCSL9PbaG+P6RAe+n
ZxZnlRoDu6grZIDsZd1UX3eccgi6GFUJxksA8YfY09Xwzeq7ZKyVz2Ab6IMVCgWY
AILj/wLl34fIGVtPXeN1GvEVt3rWboEO/l4A/ncQ/farVyPuha551B19C+8iATOO
Aj8aV4pVf3Bna/cNZ2NhDIQEVZQ2/SmccAMtLL2tGqzJX+bLZn/njWhxlRTiaHcc
M+sSnPO1/AplS29KYMH9tvsevN8HlW3D/CsqKm3rB3QnT+mCSTnP0cOhAwuz3eku
MOuxHB7/nc1ZllqBEraK7Q7dZ6SL/KF2BeajtDt6Ow8cMtTVCtK0RvC/wTQLgW2X
lzkZr6te4sMqBcQMsP6BBdHvLgkXv6LUxi4dWjhpsbwvXv3Ie/zZLjld5tECY8S0
tIGdSgSeZwRR9YEfCAn2MeT30mcDGeVtAwcjhPv4ZbQKoTSFZ40yggMPMzAutVdy
LXY7RzIZy4yk6LctYqWmDVCrf+DnMMXzwSjTBL7QIJXH9kvoCrWmYvJHXSfFixUo
E+j5Z5HmrnQZVzVkGZTuepZI5DUGCK/iPAzBATV4mp3or2oVxesTCfp0azeJiCSy
O6gHAfIoYUqJ1i61B1I4Qtbb3ro96GnoUcDUT6ekcnbNEzgue/SdG5cNgf1nsJ6Q
zYAI7ypkmEr0Wq0uFjzM
=jRpV
-----END PGP SIGNATURE-----

[ryanw...@gmail.com]

Hi Philipp,

Thanks for the quick reply. I'm quite new to the model checking world so my questions might be stupid.

I tried a more complex program attached below, if I use "-predicateAnalysis-linear -setprop solver.solver=smtinterpol" the results would be unknown and "Infeasible counterexample found, but could not remove it from the ARG.", not quite sure where went wrong.

My goal is to check if all the assertions are correct in the program, will "valueAnalysis" and "kInduction" work for this?

[Matthias Dangl]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Hi Ryan,

> My goal is to check if all the assertions are correct in the program, will "valueAnalysis" and "kInduction" work for this?

Value analysis is able to find a bug that can be replayed (i.e. confirmed) by a bit-precise predicate analysis:
  scripts/cpa.sh -preprocess -valueAnalysis noisymax.c

I also tried k-Induction, but there only the linear-arithmetic version (-kInduction-linear) finds a bug,
whereas the bit-precise version (-kInduction) ran for an hour before I gave up.

Best,
Matthias
-----BEGIN PGP SIGNATURE-----
Version: Mailvelope v2.2.2
Comment: https://www.mailvelope.com

wsFcBAEBCAAQBQJbGWP5CRDYvxoLGaFwLQAAzAQP/R1NvMbqpjv6bsVyFfn9
DgXCqLPs/USoSviEcmqPgVBwtCNHtfC95zqJlSqGsaXds9g7oOfxboRB+QWD
IsXcEnbG6M9k3YtRw1+rjd6kVk3fZ/1mmbpe0H3qwrFCaE3L6OUKZH0NUeTc
NR2HtbMugR9vZHOGUTwGs9aKx786iHMHRCgGfK8+A7KMnqL5fMKDa8v1ffWm
9wn2fR3CW9WjHbwWjkbVAiJ4FU8EIUbVmZEYus6xt6M+hI1776YU220bWsV+
R9BWNWVJ4B47m0dnl7+XyWDrLzSEqnAHUu7sXxUKOytgz8yVNiazWpxykvAh
AwJiLcnYnBlJMxiwRLULKgk0wgI8GOYJF436UutANfyQkxMmW/z8equFGLNu
WSjxyI3V73DBUljJJEgcqytoaGSiMiL5euNWFbybz0JHEpqhl5EjYBFa9Y+n
WR5mm07PugCukmuPzCCVjhL+LG04RU+dub/Tk9Z3vQs4B0Kn0Ic7tU9A+qvJ
M6H1JcBaQkyrYV+SfJx9G4MmsFSm4G1MNI/RzDEap3A3iqhto/N1KY9tlpPJ
GQIU5QPV7pU4gc4MiTpBpkOvL0V3iC9tnpy/LbOAu8T2vfPwNhkEcPZvQ4TG
e0ZBgsW+pE7AyJN5TFEdGzSnXqeL7Zcb6Vlg7tpTCkft7h7VJY8oWchUUmhy
mqXJ
=0POz
-----END PGP SIGNATURE-----

--
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-users+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.