DOMAINS :: SMT-LIB :: Announcement: first benchmarks available (and more)

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. Announcement: first benchmarks available (and more)

tinelli wrote at Apr 14, 2005 - 01:38 AM
---------------------------------------------------------------------
Dear all,

in the last few months we have been working with the SMT-COMP organizers on 
producing an initial set of benchmarks in SMT-LIB format. That has required 
a lot of work on
- addressing unresolved design issues about the format,
- defining an initial set of theories and logics,
- collecting existing benchmarks in other formats,
- translating them into the SMT-LIB format and checking their compliance
- producing some utility tools for the community
- refining the rules and the organization of SMT-COMP

We are happy to announce the results of this work:

- The SMT-LIB format, version 1.1, is now in a pretty stable form.
  You can find a detailed document on it on the SMT-LIB web site.
- A number of theory and logic definitions have been posted on the site.
  For convenience, most of the logics correspond to a division of SMT-COMP.
- A fairly large initial set of benchmarks is available from both the
  SMT-LIB and the SMT-COMP sites.
- an SMT-LIB parser and checker and a CVCL->SMT-LIB converter are now
  available from the SMT-COMP web site.
- Rules and deadlines for SMT-COMP have been finalized and a call for system
  participation and more benchmarks has been circulated (we are posting it
  in the next message in case you have not received it yet).
  
We thank the SMT-COMP organizers, Aaron Stump, Clark Barrett and Leonardo 
de Moura for their huge effort in collecting and translating the benchmarks
and in helping us refine and improve the SMT-LIB format.
We also thank those of you who have contributed one way or another to these 
achievements and we urge everybody to continue contributing by sending us more
feedback on the format, sharing additional benchmarks you might have, and
participating to SMT-COMP with your system.


Silvio & Cesare



---------------------------------------------------------------------

Reply to this message:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=164&forum=46

Browse thread:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=164

You are receiving this Email because you are subscribed to be notified of events in forums at: http://www.qpq.org/