David Wagner wrote:

Thanks for the announcement! Do you have any data on what size problems this scales to?

Dear David,

we are currently using the library for the analysis of logic and constraint logic programs. Our data-flow analyzer, when applied to the 400+ programs of our benchmark suite, never gives rise to space dimensions of more than a couple of hundreds. That is because the global inter-procedural analysis problem is partitioned in such a way that typical programs do not exceed these numbers (of course, exceptions are always possible and here is where the library being exception-safe plays an important role).

Do you have any sense for whether the library might be able to handle polyhedra with thousands of variables and tens of thousands of linear inequalities?

My feeling is that the library and the algorithms it uses do not scale that much. Of course, things may be different for problems with a particular structure, but in general the numbers you mentions seem to be out of reach. We keep improving the library though.

(I'm thinking of applications to inter-procedural program analysis for detecting security vulnerabilities.)

We also target that kind of applications. Can you give me some intuition on why scaling to thousands of variables and tens of thousands of linear constraints is necessary and/or desirable?

Regards, -- David Wagner

All the best,

Roberto Bagnara