Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Strange results when verifying bitshifts using frama-c v19.1 with z3

> How do I know if I get another false positive again?

The Frama-C/WP simplifiers are checked with an extensive base of test cases, build from community  feedback and industrial test cases.
Bitwise operations have been widely exercised during the last 5 years, but they are the more complex Frama-C simplifiers we have ever developed.
Hence, we might still find some (hopefully rare) bugs in them.

We are working on two directions to improve this situation:

1. Smoke tests: this is an automated way of trying to prove (!P) instead of P in order to detect specification inconsistencies or bugs.
2. Formally verified simplifiers: use only simplification routines that have been proved with Why-3 and Coq or SMT solvers.

We hope to release (1) during 2020 ; (2) is an on-going, long-term research work and we have an opened PhD position on this subject.

Regards,
	L.