Contacts and Contributions

For feedback, comments, and inquiries please send an email to one of co-ordinators: Clark Barrett, Pascal Fontaine, and Cesare Tinelli.

Discussion List

There is a discussion list dedicated to discussing the SMT-LIB standard and proposed extensions, as well as any other matter regarding the library: http://www.cs.nyu.edu/mailman/listinfo/smt-lib.
You can follow or join the discussion by subscribing to the list.

Benchmarks

The success of this initiative depends on collecting and maintaining a large and varied collection of benchmarks. If you would like to contribute your benchmarks to SMT-LIB please contact one of the organizers above.

Extensions

The SMT-LIB standard is driven by the needs of the community. If you would like to propose any extensions to the standard (new theories or logics, or new features for the SMT-LIB language) please contact the organizers first. For non-minor extensions, the usual process is the following:

  1. A person or group of people decides to propose an extension.
  2. They contact the organizers or they bring up the issue during the SMT-LIB discussion session at the SMT workshop.
  3. In either case, there in an initial discussion to see whether
    • the proposed extension is within the scope of the initiative and the SMT-LIB language;
    • it is of interest to enough people;
    • there are applications that would generate enough benchmarks using the extension.
  4. If the extension is deemed feasible, a work group is formed, with participation open to any interested people. At least one of the SMT-LIB co-organizers joins the work group at some point to make sure that the technical aspects of the proposal are sound.
  5. The work group discusses the extension in depth and prepares a detailed proposal.
  6. The proposal is presented to the SMT-LIB community through the discussion list above.
  7. Feedback from the community is used to improve the final version of the proposal.
  8. The proposed extension is officially incorporated into the standard and documented on this site.