[SMT-LIB] Counterexample generation in Autoactive Verification using SMT

[Martin Brain]

On Fri, 2016-07-08 at 17:01 +0200, Claude Marché wrote:
> Dear SMT-LIB list,
> 
> In the future work section of the following paper that was recently
> published in the proceedings of SEFM'2016 :
> 
>   http://link.springer.com/chapter/10.1007/978-3-319-41591-8_15
> 
> some issues are raised:
> 
> 1) lack of standard in SMT-LIB for displaying values in models found,
> especially regarding array values, and values of non-interpreted types
> 
> Is there any progress in this direction ?

As I missed SMT this year I can't comment on progress but I can observe
two (diverse) things:

A. The reason why standardisation of this is challenging is that 1. it
is tightly related to how authors represent expressions within their
solvers and 2. a common goal is that the terms in the representation
should be 'assertable' back to the solver, this, combined with things
like arrays, are what makes this hard.

B. There is nothing to stop people progressing this rather than waiting.
Come up with some goals (such as what you want to be able to do with the
terms; do you want to be able to assert them), consult with users and
authors and build something like consensus, then write a paper for the
SMT workshop proposing your solution.  I, obviously, can't guarantee
this will work but that's what we did with floating-point.

> 2) need for good candidate models even in presence of undecidable
> theories (quantifiers, resp. NIA) that should at least satisfy the
> ground part, resp. the linear part, of the input.
> 
> Such a question was discussed during a Dagstuhl seminar in October 2015,
> and a little discussion followed on the CVC mail list:
> http://cs.nyu.edu/pipermail/cvc-users/2015/000710.html
> 
> Any indeed on how this could be achieved? Soft/hard time limits as
> suggested by the paper? Any idea on achieving this using the current
> implementations of SMT solvers?

At the risk of being a bit of a stuck record; let me add a few things:

A. If you want to be able to stop the solve process at *any* point and
get some kind of useful answer, you need a solver algorithm that
provides incremental guarantees.  This is the thing I referred to as an
"Anytime" SMT algorithm.  To my knowledge, no such algorithm is known to
exist -- it is an interesting research challenge.

B. It is important to distinguish between 'unknown' answers given due to
time-out and due to incompleteness in the algorithms used.

One suggestion I made to Yannick was to use the incremental features of
the standard.  Split your problem into multiple parts and then solve
these incrementally.  For example, the first part might have all of the
ground terms.  If this is SAT you have a candidate model, if it is UNSAT
then the full formula is UNSAT.  In the SAT case you can then add the
next increment, for example, the quantified statements and solve again.
If this hits the time limit then you still have the candidate model.  If
the first increment is small enough you will almost always get the model
you need with minimal extra overhead.

HTH

Cheers,
 - Martin