--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on May 2020 ---
[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