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] New user questions

Hello Mike,

>  
> For different solvers, I get different answers from alt-ergo and z3 for the same properties, with z3 timing out or failing on a handful of goals that alt-ergo succeeds on.  I would expect differences in timeouts between solvers (e.g., one times out but not the other), but not discrepancies as to whether obligations are true or false.  Perhaps ‘failure’ in this case simply means ‘failure to prove’.  I am running z3 4.8.4 and alt-ergo 2.3.2. 

It is very important to understand and accept that in general, as you suspect, ‚failure‘ means 'failure to prove‘.
This is related to very fundamental facts about mathematical logic and computer science and constitutes one of the greatest
scientific achievements of the 20th century.
I just link to this paragraph of a wikipedia article on automated theorem probing 
    https://en.wikipedia.org/wiki/Automated_theorem_proving#Decidability_of_the_problem

The book "Logic in Computer Science: Modelling and Reasoning about Systems“ by Michael Huth and Mark Ryan
also has a short section about this topic.
(The book is is available at Amazon: https://www.amazon.com/Logic-Computer-Science-Modelling-Reasoning/dp/052154310X)

Regards

Jens