[SMT-LIB] you questions on SMT-LIB

[Domagoj Babic]

Hi Cesare,

Sorry for the slow response, I'm swamped with work...

Cesare Tinelli wrote:
>> The other related point is just pure readability. It is not really
>> obvious what (/ 80143857 25510582) or (+ 3 (/ 1 (7 + (/ 1 16))))
>> stands for.
>>
> Let me stress this once more, for everybody. The SMT-LIB format is meant
> to be an intermediate format, mostly for machine use. Human readability
> is not the driving concern.

IMHO, disregarding readibility is a suboptimal design decision. Makes
the debugging and development of the decision procedures harder.

>> Finally, the benchmark generators would need to come up with
>> these approximations, and the decision procedures need to perform
>> additional redundant divisions, which is a problem from both
>> precision and performance point of view.
>>
> Yes, but again this means that we are not using the right logic for
> those benchmarks and we should develop a mathematical (meta)theory of
> floating point numbers (axiomatization, determination of the
> decidability of the SMT problem, sound a complete satisfiability
> algorithms and so on).
> Except for the axiomatization (done by the Maude people,
> http://maude.cs.uiuc.edu/) I'm not aware of the existence of such work.
> Are you, or anyone in the list, aware of such results?

Sorry, no. I can ask around. My guess is that people working on
hybrid-systems verification might have developed something along those
lines.

>> Perhaps my comment is of-the-track. But, what is the purpose of LRA
>> if it cannot exactly model the floating point behaviour commonly
>> found in HW & SW systems?
>>
> Your question is in fact right on track. The answer is: the point of LRA
> for HW & SW verification is that it can used to do *approximate*
> reasoning over the floating point numbers. We use LRA at the moment
> because we do not have better options, yet.
>
> As research advances, we will hopefully arrive to an accurate theory and
> logic of floating point numbers, and finally use that one for HW & SW
> verification.
>
> The same point can be made about integer arithmetic of course. That is
> why I look forward to research like your own on reasoning about machine
> ints, not mathematical integers. Until then Presburger arithmetic will
> have to do.

Okay. That makes sense. The comment also explains the choice of
the representation of constants.

>> I'd suggest asking
>> Byron Cook. In a month-or-two, I'm going to generate a set of modular
>> arithmetic SW verification benchmarks (too late for SMT'06). Also,
>> I'll have my own decision procedure (unrelated to the work I did
>> with Madan) by autumn.
>>
>> BTW, what's the current status of the QF_MLIA spec?
>>
>> If the spec is nonexisting, or in a very nascent state, I'd be
>> interested to get involved in its development for SMT'07.
>>
> Great. Let's keep in touch on that.

Sure. The first batch of benchmarks will be in annotated (but otherwise
fully-compatible) DIMACS CNF format. Depending on how the progress on
QF_MLIA will go, I can generate the second batch in QF_MLIA or something
similar...

All my tools (the interprocedural SW analysis, expression simplifier, and
the decision procedure) exchange information in an efficient internal
format, but it would be nice to have some standardized format (like
QF_MLIA), at least for debugging and comparison [That's why I care about
the readability of the format too.].

After I get the first benchmarks in the CNF form, I'll let you know.
My guess is that that will happen in a month or two. Everything got
delayed a bit because I was working on my proposal (which is almost
finished) and on the interprocedural SW analysis for generating VCs
(which is also almost done).

The benchmarks will correspond to verification conditions from several
open-source applications. It's very likely that the first batch of
benchmarks will check only a very limited set of properties. This shouldn't
matter that much because the structure of the original code will be
maintained.

Regards,
    Domagoj Babic