DOMAINS :: SMT-LIB :: News from PDPAR'04 and CAV'04

[Ofer Strichman]

As for the workshop next year: if there will be two days of workshops, it is
better to have it not on the same day of the BMC'05 workshop (and probably
others which I don't know about yet) as the sets of interested people in
these workshops is not mutually exclusive.

Ofer




----- Original Message ----- 
From: "QPQ" <saadati at csl.sri.com>
To: <smt-disc at cs.uiowa.edu>
Sent: Monday, July 26, 2004 3:22 PM
Subject: DOMAINS :: SMT-LIB :: News from PDPAR'04 and CAV'04


> Forums QPQ
> DOMAINS :: SMT-LIB ::.. News from PDPAR'04 and CAV'04
>
> tinelli wrote at Jul 26, 2004 - 02:22 PM
> ---------------------------------------------------------------------
> As some of you already know, the last editions of PDPAR, held in Cork,
Ireland last July had a panel on SMT-LIB. Many of the SMT people
(re)convened the following week at CAV in Boston, and further discussed
SMT-LIB issues.
> Here is a brief account of the main points discussed at PDPAR and CAV.
>
> 1. Version 1.0 of SMT-LIB format
> 2. XML support for SMT-LIB
> 3. SMT System Competition
> 4. Next PDPAR
>
>
> 1.
> At the panel, Cesare and Silvio briefly reported on the past work on
SMT-LIB, including that on a recently submitted NSF proposal, and then
presented Version 1.0 of the SMT-LIB format. A preliminary drat of the
document defining Version one was distributed to the panel participants.
>
> 2.
> A proposal by Filip Maric and Predrag Janicic was discused of using XML as
a basis for SMT-LIB. Their original proposal was submitted to PDPAR'04 and
is included in the workshop's proceedings, available from PDPAR's website
(http://www.loria.fr/~ranise/pdpar04/).
> Filip and Predrag propose to use XML and MathML as the underlying format
for storing theories and benchmarks within the SMT-LIB library, as opposed
to a raw, plain text representation. You can check the PDPAR proceedings for
the rationale of the proposal (they are what you would expect).
> The recommendation coming out of the panel discussion was that it was fine
to store SMT-LIB data internally in XML and MathML format, as long as
translators from and into the actual SMT-LIB format (as defined in Version
1) were developed and made available, so that tool developers could use just
the SMT-LIB format if they chose to.
> We plan on following this recommendation and work with Filip and Predrag
on creating the needed XML infrastructure (DTDs, XSLT style sheets, SMT-LIB
converters and on) based on the work they have already done.
>
> 3.
> To help SMT-LIB gain momentum and start collecting benchmarks from the
community in the SMT-LIB format, Alessandro Armando proposed to create an
SMT system competition, modeled after similar competitions for SAT solvers
(http://www.satlive.org/SATCompetition/) or first-order theorem provers
(http://www.cs.miami.edu/~tptp/CASC/).
> The proposal was received enthusiastically by the panel participants, and
by several more people in our community later at CAV.
> Aaron Stump and Clark Barrett agreed on organizing the first edition of
the competion. They were later joined by Leonardo de Moura, who has
accumulated quite a lot of experience in comparing SMT systems recently, as
illustrated in his nice paper at CAV'04 with Harald Ruess.
> More information on the SMT competition and how you can participate with
your system, and contribute to with your benchmarks will be posted in the
next few months. Stay tuned!
>
> 4.
> Given the success of PDPAR'04 and on the strong interest for decision
procedures and SMT systems in general shown at IJCAR and CAV this year, it
has been decided to have another edition next year.
> Alessandro Armando and Alessandro Cimatti have agreed to organize it.
Based on the very positive feedback received at PDPAR and CAV, the workshop
will be proposed as a satellite workshop of CAV'05, to be held in Edinburgh,
Scotland next July.
> The SMT system competition will be also proposed for CAV'05.
> Cesare and Alessandro (Cimatti) have already spoken with the program and
local chairs of CAV'05 about this. They have expressed strong interest in
both the workshop and the competition, promising logistical and plenty of
harware support for the latter.
> We will keep you posted on this as well.
>
> Best,
>
>
> Silvio & Cesare
>
>
>
> ---------------------------------------------------------------------
>
> Reply to this message:
>
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=47&forum=46
>
> Browse thread:
>
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=47
>
> You are receiving this Email because you are subscribed to be notified of
events in forums at: http://www.qpq.org/
>