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

[QPQ]

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/