AISB Convention 2015

Call for Symposium Proposals: The AISB Convention is an annual conference covering the range of AI and Cognitive Science, organised by the Society for the Study of Artificial Intelligence and Simulation of Behaviour. The 2015 Con...


Read More...

Yasemin Erden on BBC

AISB Committee member, and Philosophy Programme Director and Lecturer, Dr Yasemin J. Erden interviewed for the BBC on 29 October 2013. Speaking on the Today programme for BBC Radio 4, as well as the Business Report for BBC world N...


Read More...

Mark Bishop on BBC ...

Mark Bishop, Chair of the Study of Artificial Intelligence and the Simulation of Behaviour, appeared on Newsnight to discuss the ethics of ‘killer robots’. He was approached to give his view on a report raising questions on the et...


Read More...

AISB YouTube Channel

The AISB has launched a YouTube channel: http://www.youtube.com/user/AISBTube (http://www.youtube.com/user/AISBTube). The channel currently holds a number of videos from the AISB 2010 Convention. Videos include the AISB round t...


Read More...

Lighthill Debates

The Lighthill debates from 1973 are now available on YouTube. You need to a flashplayer enabled browser to view this YouTube video  


Read More...
01234

Notice

AISB event Bulletin Item

Announcing SMT-COMP 2008: Satisfiability Modulo Theories Competition

http://www.smtcomp.org/

CAV'08 Satellite Event

       4th International Satisfiability Modulo Theories Competition
                               (SMT-COMP'08)

                              Princeton, USA
                                 July 2008

                            CALL FOR BENCHMARKS
                             CALL FOR ENTRANTS

======================================================================

Decision procedures for checking satisfiability of logical formulas
are crucial for many verification applications.  Of particular recent
interest are solvers for Satisfiability Modulo Theories (SMT).
SMT-COMP aims to spur innovation in SMT research by providing a yearly
friendly competition for SMT solvers.

SMT-COMP came out of discussions surrounding the SMT-LIB initiative,
an initiative of the SMT community to build a library of SMT
benchmarks in a proposed standard format.  SMT-COMP helps serve this
goal by contributing collected benchmark formulas used for the
competition to the library, and by providing an incentive for
implementors of SMT solvers to support the SMT-LIB format.

As part of SMT-COMP 2007, a special session was held at SMT Workshop
2007 in which the competitors had a chance to present their tools and
discuss them with other competitors.  This year, a similar session
will be held as part of SMT Workshop 2008 (July 7-8, affiliated with
CAV).  More information about the SMT Workshop can be found on the web
page: http://research.microsoft.com/conferences/SMT08/

The highlights of SMT-COMP 2008 are covered below.  For the latest
information, please see the SMT-COMP web page at:

http://www.smtcomp.org/

------------------------------------------
Main changes with respect to SMT-COMP 2007
------------------------------------------

- Use of the SMT-EXEC services for solver submission and execution

- Updates to the benchmark selection algorithms

- Additional mechanisms for transparency and reproducibility of results

- Existence of a two-day grace period for bug fixing

For more detailed information please refer to the rules posted at
http://www.smtcomp.org/.

---------------
Benchmarks
---------------

The potential benchmark divisions for this year include all of the
divisions represented last year. We do not anticipate new divisions
this year unless quality benchmarks are collected. For detailed
descriptions of the divisions, refer to the SMT-LIB web page at
http://www.smtlib.org/

* QF_UF (Uninterpreted Functions): quantifier-free formulas whose
  satisfiability is to be decided modulo the empty theory. Each
  benchmark may introduce its own uninterpreted function and predicate
  symbols.

* QF_IDL (Integer Difference Logic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  The syntax of atomic formulas is restricted to
  difference logic, i.e. x - y op c, where op is either equality or
  inequality and c is an integer constant.

* QF_RDL (Real Difference Logic): this division is like QF_IDL, except
  that the background theory is real arithmetic.

* QF_UFIDL (Integer Difference Logic with Uninterpreted Functions):
  this division contains benchmarks in a logic which is similar to
  QF_IDL, except that it also allows uninterpreted functions and
  predicates.

* QF_LIA (Linear Integer Arithmetic): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of integer
  arithmetic.  The syntax of atomic formulas is restricted to contain
  only linear terms.

* QF_LRA (Linear Real Arithmetic): this division is like QF_LIA,
  except that the background theory is real arithmetic.

* QF_UFLIA (Linear Integer Arithmetic with Uninterpreted Functions):
  this division contains benchmarks in a logic which is similar to
  QF_LIA, except that it also allows uninterpreted functions and
  predicates.

* QF_AX (Arrays with Extensionality): quantifier-free formulas to be
  tested for satisfiability modulo a background theory of arrays which
  includes the extensionality axiom.

* QF_AUFLIA (Linear Integer Arithmetic with Uninterpreted Functions
  and Arrays): quantifier-free formulas to be tested for
  satisfiability modulo a background theory combining linear integer
  arithmetic, uninterpreted function and predicate symbols, and
  extensional arrays.

* QF_BV (Fixed-size Bit-vectors): quantifier-free formulas over bit
  vectors of fixed size.

* QF_AUFBV (Bit-vectors with Arrays and Uninterpreted Functions):
  quantifier-free formulas over bit vectors of fixed size, with arrays
  and unintepreted functions and predicate symbols.

* AUFLIA+p (Linear Integer Arithmetic with Uninterpreted Functions and
  Arrays): quantified formulas to be tested for satisfiability modulo
  a background theory combining linear integer arithmetic,
  uninterpreted function and predicate symbols, and extensional
  arrays. Benchmarks include patterns for guiding instantiation
  mechanisms.

* AUFLIA-p (Linear Integer Arithmetic with Uninterpreted Functions and
  Arrays): formulas from AUFLIA+p once all patterns have been
  removed.

* AUFLIRA+p (Arrays, Uninterpreted Functions, and Linear Arithmetic):
  quantifier formulas with arrays of reals indexed by integers
  (Array1), arrays of Array1 indexed by integers (Array2), and linear
  arithmetic over the integers and reals. Benchmarks include patterns
  for guiding instantiation mechanisms.

* AUFLIRA-p (Arrays, Uninterpreted Functions, and Linear Arithmetic):
  formulas from AUFLIRA+p once all patterns have been removed.

As with last year, we reserve the right to remove benchmark divisions
if we do not receive enough quality benchmarks or enough solvers in a
particular division.  If you have access to benchmarks in any of these
divisions, even if they are not in the SMT-LIB format, please contact
one of the organizers (see below).

---------------
Solvers
---------------

Please refer to http://www.smtcomp.org/ for complete details on
entering the competition.

---------------
Travel Grants
---------------

Microsoft Research has generously donated funds to help pay for travel
for participants, especially students, who might otherwise be unable
to attend. Because funds are limited, we will use a bidding process to
assign grants. The process works like this:

 1. Those interested should send an email by June 1 to Clark Barrett 
 indicating:
    * Your name and affiliation.
    * Whether you are a student.
    * The name of the solver you are submitting and your role in the 
    development of the solver.
    * The amount of assistance you would need to be able to attend. 

 2. On or before June 11, we will notify those whose bids have been
    accepted (acceptance will be based primarily on the amount
    requested, with lower bids having precedence, but we will also
    take into account the role of the applicant in the development of
    the solver and whether or not the applicant is a student).

 3. Following the conclusion of the competition, reimbursement checks
    will be issued to those whose bids were accepted and who attended.


---------------
Important Dates
---------------

    * May 1:     First version of the benchmark library posted for 
                 comment.

    * June 1:    Revised version of the benchmark library posted.
      	    	 Travel grant applications due.

    * June 11:   Travel grant notification sent.

    * July 4:    Final version of solvers due via SMT-EXEC,with magic 
     (7pm ET)	 numbers for pseudo-random selection of benchmarks.

    * July 6:    Close of two-day grace period for resubmission of 
     (7pm ET) 	 entries.

    * July 7-8:  SMT Workshop.

    * July 9-13: Anticipated dates for competition.


-----------------
Organizers
-----------------

Clark Barrett   (New York University, barrett@cs.nyu.edu)
Morgan Deters   (Technical Univ. of Catalonia, mdeters@lsi.upc.edu)
Albert Oliveras (Technical Univ. of Catalonia, oliveras@lsi.upc.edu)
Aaron Stump     (Washington University in St. Louis, stump@cse.wustl.edu)

----------------
More Information
----------------

For details on the competition, see
http://www.smtcomp.org/

For more information on the SMT-LIB format, see
http://www.smtlib.org/

For more information about the SMT Workshop, see
http://research.microsoft.com/conferences/SMT08/

SMT-COMP is partially sponsored by the U.S. National Science Foundation, under
grant CNS-0551697.